The Dual Lattice

In this file, we build some basic theory about the dual lattice of a given ZLattice. We build on API developed by Andrew Yang in Mathlib.LinearAlgebra.BilinearForm.DualLattice. We show that the dual lattice with respect to a nondegenerate bilinear form on a lattice is itself a lattice, which will allow us to construct an isomorphism with the canonical free ℤ-module of its rank.

Note that parts of this file can probably be generalised to RCLike 𝕜. We do not do this here.

Main Definition

ZLattice.Dual: The dual of a ZLattice as a ℤ-submodule.

Main Results

1. ZLattice.Dual.eq_Zspan : The dual of a ZLattice is the ℤ-span of its associated dual basis.
2. ZLattice.Dual.instZLattice : The dual of a ZLattice is itself a ZLattice.

noncomputable def ZLattice.Dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (B : LinearMap.BilinForm ℝ E) (Λ : Submodule ℤ E) : Submodule ℤ E

The dual of a ZLattice is its dual as a ℤ-submodule.

Equations

• ZLattice.Dual B Λ = B.dualSubmodule Λ

theorem ZLattice.Dual.eq_ZSpan {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (B : LinearMap.BilinForm ℝ E) (hB : B.Nondegenerate) (Λ : Submodule ℤ E) [hdiscrete : DiscreteTopology ↥Λ] [hlattice : IsZLattice ℝ Λ] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι ℤ ↥Λ) : Dual B Λ = Submodule.span ℤ (Set.range ⇑(B.dualBasis hB (Module.Basis.ofZLatticeBasis ℝ Λ b)))

The dual of a ZLattice is the ℤ-span of the dual basis of its ofZLatticeBasis.

instance ZLattice.Dual.instDiscreteTopology {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (B : LinearMap.BilinForm ℝ E) (hB : B.Nondegenerate) (Λ : Submodule ℤ E) [hdiscrete : DiscreteTopology ↥Λ] [hlattice : IsZLattice ℝ Λ] : DiscreteTopology ↥(Dual B Λ)

The dual of a ZLattice has the discrete topology.

instance ZLattice.Dual.instIsZLattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (B : LinearMap.BilinForm ℝ E) (hB : B.Nondegenerate) (Λ : Submodule ℤ E) [hdiscrete : DiscreteTopology ↥Λ] [hlattice : IsZLattice ℝ Λ] [DiscreteTopology ↥(Dual B Λ)] : IsZLattice ℝ (Dual B Λ)

The dual of a ZLattice is itself a ZLattice.