Documentation

SpherePacking.ForMathlib.PoissonSummation.DualLattice

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.
source
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
Instances For
    source
    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 : Basis ι ℤ ↥Λ) :
    Dual B Λ = Submodule.span ℤ (Set.range ⇑(B.dualBasis hB (Basis.ofZLatticeBasis ℝ Λ b)))

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

    source
    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.

    source
    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.