The dual lattice in a real inner product space

For a ℤ-submodule L of a real inner product space E, the dual lattice

L^∨ = {x ∈ E | ⟪x, y⟫ ∈ ℤ for all y ∈ L}

is Mathlib's BilinForm.dualSubmodule of the inner product innerₗ E, with ℤ as the ring of coefficients. This file names that submodule ZLattice.dual and develops the part of its theory that holds for a full lattice in a finite-dimensional space: the dual of a full lattice is again a full lattice (ZLattice.dual carries DiscreteTopology and IsZLattice instances), and taking the dual twice gives the lattice back (ZLattice.dual_dual).

Both facts come from the dual-basis description of Mathlib: the dual of the ℤ-span of an ℝ-basis b is the ℤ-span of the basis dual to b for the inner product (ZLattice.dual_span_basis), and a full lattice is the ℤ-span of an ℝ-basis. In particular the ℤ-span of an orthonormal basis is its own dual (ZLattice.dual_span_orthonormalBasis), the self-duality of ℤⁿ ⊆ ℝⁿ.

The dual is antitone, and it commutes with pulling a lattice back along a linear isometry equivalence (ZLattice.dual_comap), so every notion defined from it is an isometry invariant. Along a general continuous linear equivalence e of complete spaces the dual is pulled back along the adjoint of e⁻¹ instead (ZLattice.dual_comap_continuousLinearEquiv): the dual of A L is (A⁻¹)ᵀ L^∨, the transport of dual lattices under a linear change of variables.

This is the dual lattice entering Poisson summation over a lattice, and the integrality, evenness and unimodularity of a lattice in TauCeti/Algebra/Module/ZLattice/Integral.lean are defined from it.

Main definitions

• ZLattice.dual L: the dual of L : Submodule ℤ E with respect to the inner product.
• ZLattice.basisSpanOrthonormalBasis b: an orthonormal basis b as a ℤ-basis of its ℤ-span.
• ZLattice.dualComapEquiv L e: the ℤ-linear equivalence (e⁻¹ L)^∨ ≃ₗ[ℤ] L^∨ induced by a linear isometry equivalence e.

Notation

• L^∨: the dual lattice ZLattice.dual L, scoped in ZLattice.

Main statements

• ZLattice.mem_dual: x ∈ dual L if and only if ⟪x, y⟫ is an integer for every y ∈ L.
• ZLattice.dual_span_basis: the dual of the ℤ-span of an ℝ-basis is the ℤ-span of its dual basis.
• ZLattice.dual_span_orthonormalBasis: the ℤ-span of an orthonormal basis is self-dual.
• ZLattice.dual_span_singleton: the dual of c ℤ ⊆ ℝ (c ≠ 0) is c⁻¹ ℤ.
• ZLattice.inf_dual_span_singleton_eq_bot_of_irrational_sq: when c² is irrational, c ℤ ⊆ ℝ meets its dual c⁻¹ ℤ only at 0.
• ZLattice.dual_dual: the dual of the dual of a full lattice is the lattice itself.
• ZLattice.dual_comap: the dual commutes with pulling back along a linear isometry equivalence.
• ZLattice.dual_comap_continuousLinearEquiv: the dual of the pullback along a continuous linear equivalence e is the pullback of the dual along the adjoint of e⁻¹.

noncomputable def ZLattice.dual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : Submodule ℤ E

The dual lattice of L : Submodule ℤ E: the vectors whose inner product with every vector of L is an integer. It is Mathlib's BilinForm.dualSubmodule of the inner product.

def ZLattice.«term_^∨» : Lean.TrailingParserDescr

The dual lattice of L : Submodule ℤ E: the vectors whose inner product with every vector of L is an integer. It is Mathlib's BilinForm.dualSubmodule of the inner product.

theorem ZLattice.dual_def {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : dual L = LinearMap.BilinForm.dualSubmodule (innerₗ E) L

@[simp]

theorem ZLattice.mem_dual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} {x : E} : x ∈ dual L ↔ ∀ y ∈ L, ∃ (m : ℤ), inner ℝ x y = ↑m

A vector lies in the dual lattice exactly when its inner product with every vector of L is an integer.

theorem ZLattice.dual_anti {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L M : Submodule ℤ E} (h : L ≤ M) : dual M ≤ dual L

Taking duals reverses inclusions.

theorem ZLattice.le_dual_comm {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L M : Submodule ℤ E} : L ≤ dual M ↔ M ≤ dual L

L lies in the dual of M if and only if M lies in the dual of L: both say that L and M pair integrally.

theorem ZLattice.le_dual_dual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : L ≤ dual (dual L)

Every lattice is contained in the dual of its dual. Equality holds for a full lattice in a finite-dimensional space, dual_dual.

theorem ZLattice.dual_span_basis {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Finite ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) : dual (Submodule.span ℤ (Set.range ⇑b)) = Submodule.span ℤ (Set.range ⇑(LinearMap.BilinForm.dualBasis (innerₗ E) ⋯ b))

The dual of the ℤ-span of an ℝ-basis is the ℤ-span of the dual basis for the inner product.

instance ZLattice.instDiscreteTopologySpanOrthonormalBasis {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑b))

The ℤ-span of an orthonormal basis is discrete, as the ℤ-span of the underlying basis b.toBasis is.

instance ZLattice.instIsZLatticeSpanOrthonormalBasis {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑b))

The ℤ-span of an orthonormal basis is a full lattice, a copy of ℤⁿ ⊆ ℝⁿ.

noncomputable def ZLattice.basisSpanOrthonormalBasis {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : Module.Basis ι ℤ ↥(Submodule.span ℤ (Set.range ⇑b))

An orthonormal basis b is a ℤ-basis of its ℤ-span ℤ b.

@[simp]

theorem ZLattice.coe_basisSpanOrthonormalBasis_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) (i : ι) : ↑((basisSpanOrthonormalBasis b) i) = b i

The i-th vector of the ℤ-basis basisSpanOrthonormalBasis b of ℤ b is b i.

@[simp]

theorem ZLattice.dual_span_orthonormalBasis {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : dual (Submodule.span ℤ (Set.range ⇑b)) = Submodule.span ℤ (Set.range ⇑b)

The ℤ-span of an orthonormal basis is its own dual.

theorem ZLattice.dual_span_singleton {c : ℝ} (hc : c ≠ 0) : dual (ℤ ∙ c) = ℤ ∙ c⁻¹

The dual of the rank-one lattice c ℤ ⊆ ℝ (c ≠ 0) is c⁻¹ ℤ.

theorem ZLattice.inf_dual_span_singleton_eq_bot_of_irrational_sq {c : ℝ} (hc : Irrational (c ^ 2)) : ℤ ∙ c ⊓ dual (ℤ ∙ c) = ⊥

When c² is irrational, the rank-one lattice c ℤ ⊆ ℝ meets its dual c⁻¹ ℤ only at 0.

@[simp]

theorem ZLattice.dual_comap {E : Type u} {F : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) : dual (ZLattice.comap ℝ L ↑e.toLinearEquiv) = ZLattice.comap ℝ (dual L) ↑e.toLinearEquiv

The dual commutes with pulling a lattice back along a linear isometry equivalence.

noncomputable def ZLattice.dualComapEquiv {E : Type u} {F : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) : ↥(dual (ZLattice.comap ℝ L ↑e.toLinearEquiv)) ≃ₗ[ℤ] ↥(dual L)

A linear isometry equivalence e : F ≃ₗᵢ[ℝ] E identifies the dual of the pullback of L with the dual of L.

@[simp]

theorem ZLattice.coe_dualComapEquiv_apply {E : Type u} {F : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) (x : ↥(dual (ZLattice.comap ℝ L ↑e.toLinearEquiv))) : ↑((dualComapEquiv L e) x) = e ↑x

Applying dualComapEquiv L e applies e to the underlying vector.

@[simp]

theorem ZLattice.coe_dualComapEquiv_symm_apply {E : Type u} {F : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) (y : ↥(dual L)) : ↑((dualComapEquiv L e).symm y) = e.symm ↑y

Applying (dualComapEquiv L e).symm applies e.symm to the underlying vector.

@[simp]

theorem ZLattice.dual_comap_continuousLinearEquiv {E : Type u} {F : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (L : Submodule ℤ E) (e : F ≃L[ℝ] E) : dual (ZLattice.comap ℝ L ↑↑e) = ZLattice.comap ℝ (dual L) ↑(ContinuousLinearMap.adjoint ↑e.symm)

The dual of the pullback of a lattice along a continuous linear equivalence e is the pullback of the dual along the adjoint of e⁻¹. Read through images, the dual of A L is (A⁻¹)ᵀ L^∨ for a linear automorphism A.

instance ZLattice.instDiscreteTopologySubtypeMemSubmoduleIntDual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] : DiscreteTopology ↥(dual L)

instance ZLattice.instIsZLatticeRealDual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] : IsZLattice ℝ (dual L)

@[simp]

theorem ZLattice.dual_dual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] : dual (dual L) = L

The dual of the dual of a full lattice in a finite-dimensional space is the lattice.