Duals of integral lattices

For an integral lattice L in a rational vector space with nondegenerate form, its dual carrier is the submodule

Lᵛ = {x | B(x, y) ∈ ℤ for every y ∈ L}.

This file keeps the dual as a submodule of the same rational ambient space. It is not packaged as an IntegralLattice: the restriction of the form to Lᵛ need not be integral. For example, the dual of the rank-one lattice of Gram matrix (2) has Gram matrix (1 / 2).

Mathlib proves that the dual of the integral span of a rational basis is the integral span of the bilinear dual basis. Applying that result to the basis supplied by Submodule.IsLattice proves that Lᵛ is again a full lattice. It also identifies the natural pairing map Lᵛ → Module.Dual ℤ L as an equivalence and proves reflexivity (Lᵛ)ᵛ = L.

Main declarations

• TauCeti.IntegralLattice.dualCarrier: the dual lattice as a submodule of the common ambient rational vector space.
• TauCeti.IntegralLattice.le_dualCarrier: the inclusion L.carrier ≤ L.dualCarrier.
• TauCeti.IntegralLattice.instIsLatticeDualCarrier: the dual carrier is a full lattice.
• TauCeti.IntegralLattice.finrank_dualCarrier: the dual carrier has the same rank as the ambient rational space.
• TauCeti.IntegralLattice.dualPairing: the pairing of a dual-lattice vector with a lattice vector, valued in ℤ.
• TauCeti.IntegralLattice.dualPairingEquiv: the perfect integral pairing Lᵛ ≃ Module.Dual ℤ L.
• TauCeti.IntegralLattice.dualBasisElem: embedding of a bilinear dual-basis vector into the dual carrier.
• TauCeti.IntegralLattice.dualCarrierBasis: the dual basis of L.dualCarrier corresponding to a chosen basis of L.carrier.
• TauCeti.IntegralLattice.dualSubmodule_flip_dualCarrier: double duality with form.flip.
• TauCeti.IntegralLattice.dualSubmodule_dualCarrier: dualizing twice recovers L.
• TauCeti.IntegralLattice.Isometry.map_dualCarrier_ambientEquiv: an isometry maps the dual carrier onto the dual carrier.
• TauCeti.IntegralLattice.Isometry.dualCarrierEquiv: transport of dual carriers by an isometry.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md (Layer 2)
• TauCetiRoadmap/IntegralLattices/Suggested.lean

@[reducible, inline]

abbrev TauCeti.IntegralLattice.dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule ℤ V

The dual carrier of an integral lattice: x belongs to it exactly when L.form x y is integral for every y ∈ L.

Equations

• L.dualCarrier = L.form.dualSubmodule L.carrier

theorem TauCeti.IntegralLattice.le_dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.carrier ≤ L.dualCarrier

The carrier of an integral lattice is contained in its dual carrier.

theorem TauCeti.IntegralLattice.dualCarrier_eq_span_dualBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) : L.dualCarrier = Submodule.span ℤ (Set.range ⇑(L.form.dualBasis ⋯ (Module.Basis.extendOfIsLattice ℚ b)))

The dual carrier is the integral span of the bilinear dual basis to the rational basis extending any ℤ-basis of the carrier.

instance TauCeti.IntegralLattice.instIsLatticeDualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : Submodule.IsLattice ℚ L.dualCarrier

The dual carrier of a nondegenerate integral lattice is a full lattice in the same rational ambient space.

theorem TauCeti.IntegralLattice.finrank_dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : Module.finrank ℤ ↥L.dualCarrier = Module.finrank ℚ V

The dual carrier has the same rank as the ambient rational space.

noncomputable def TauCeti.IntegralLattice.dualPairing {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↥L.dualCarrier →ₗ[ℤ] Module.Dual ℤ ↥L.carrier

The pairing of a dual-lattice vector with a lattice vector, valued in ℤ.

Equations

• L.dualPairing = L.form.dualSubmoduleToDual L.carrier

@[simp]

theorem TauCeti.IntegralLattice.dualPairing_cast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.dualCarrier) (y : ↥L.carrier) : ↑((L.dualPairing x) y) = (L.form ↑x) ↑y

The integral dual pairing becomes the ambient rational form after casting to ℚ.

noncomputable def TauCeti.IntegralLattice.dualPairingEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : ↥L.dualCarrier ≃ₗ[ℤ] Module.Dual ℤ ↥L.carrier

The pairing with the carrier is perfect: every integral functional on L is represented by a unique vector of Lᵛ.

Equations

• L.dualPairingEquiv = L.form.dualSubmoduleEquivDual ⋯ L.carrier

@[simp]

theorem TauCeti.IntegralLattice.dualPairingEquiv_toLinearMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : ↑L.dualPairingEquiv = L.dualPairing

The perfect pairing equivalence has dualPairing as its underlying linear map.

@[simp]

theorem TauCeti.IntegralLattice.dualPairingEquiv_cast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (x : ↥L.dualCarrier) (y : ↥L.carrier) : ↑((L.dualPairingEquiv x) y) = (L.form ↑x) ↑y

The perfect pairing equivalence agrees with the ambient rational form after casting to ℚ.

noncomputable def TauCeti.IntegralLattice.dualBasisElem {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) (i : ι) : ↥L.dualCarrier

A vector of the bilinear dual basis corresponding to an arbitrary carrier basis, regarded as an element of the dual carrier.

Equations

• L.dualBasisElem b i = ⟨(L.form.dualBasis ⋯ (Module.Basis.extendOfIsLattice ℚ b)) i, ⋯⟩

@[simp]

theorem TauCeti.IntegralLattice.coe_dualBasisElem {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) (i : ι) : ↑(L.dualBasisElem b i) = (L.form.dualBasis ⋯ (Module.Basis.extendOfIsLattice ℚ b)) i

The underlying rational vector of dualBasisElem is the corresponding vector of the bilinear dual basis.

@[simp]

theorem TauCeti.IntegralLattice.dualPairingEquiv_dualBasisElem {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) (i : ι) : L.dualPairingEquiv (L.dualBasisElem b i) = b.dualBasis i

Under the perfect-pairing equivalence, the bilinear dual basis of the ambient space is sent to the module-dual basis of the carrier.

noncomputable def TauCeti.IntegralLattice.dualCarrierBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) : Module.Basis ι ℤ ↥L.dualCarrier

The basis of the dual carrier corresponding to a ℤ-basis of L.carrier.

Equations

• L.dualCarrierBasis b = b.dualBasis.map L.dualPairingEquiv.symm

@[simp]

theorem TauCeti.IntegralLattice.dualCarrierBasis_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) (i : ι) : (L.dualCarrierBasis b) i = L.dualBasisElem b i

The basis of the dual carrier corresponding to a ℤ-basis b consists of the ambient bilinear dual-basis vectors.

@[simp]

theorem TauCeti.IntegralLattice.dualCarrierBasis_repr {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) (x : ↥L.dualCarrier) : (L.dualCarrierBasis b).repr x = b.dualBasis.repr (L.dualPairingEquiv x)

Coordinates in the dual-carrier basis are evaluations of the perfect pairing on the original carrier basis.

theorem TauCeti.IntegralLattice.dualSubmodule_flip_dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : L.form.flip.dualSubmodule L.dualCarrier = L.carrier

Taking the flipped dual submodule of the dual carrier recovers the original carrier.

@[simp]

theorem TauCeti.IntegralLattice.dualSubmodule_dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : L.form.dualSubmodule L.dualCarrier = L.carrier

Taking the dual submodule twice recovers the original carrier.

theorem TauCeti.IntegralLattice.forall_form_mem_one_dualCarrier_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (x : V) : (∀ y ∈ L.dualCarrier, (L.form x) y ∈ 1) ↔ x ∈ L.carrier

A vector pairs integrally with every vector of the dual carrier exactly when it belongs to the original carrier.

theorem TauCeti.IntegralLattice.Isometry.apply_mem_dualCarrier_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : V) : e x ∈ M.dualCarrier ↔ x ∈ L.dualCarrier

An isometry carries an ambient vector into the target dual carrier exactly when the original vector belongs to the source dual carrier.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.map_dualCarrier_ambientEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : Submodule.map (↑e.ambientEquiv) L.dualCarrier = M.dualCarrier

The ambient integral equivalence of an isometry maps the source dual carrier onto the target dual carrier.

def TauCeti.IntegralLattice.Isometry.dualCarrierEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ↥L.dualCarrier ≃ₗ[ℤ] ↥M.dualCarrier

An isometry restricts to an integral linear equivalence of dual carriers.

Equations

• e.dualCarrierEquiv = e.ambientEquiv.ofSubmodules L.dualCarrier M.dualCarrier ⋯

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_dualCarrierEquiv_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : ↥L.dualCarrier) : ↑(e.dualCarrierEquiv x) = e ↑x

The dual-carrier equivalence acts by the underlying ambient isometry.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.dualCarrierEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).dualCarrierEquiv = LinearEquiv.refl ℤ ↥L.dualCarrier

The dual-carrier restriction of the identity isometry is the identity equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.dualCarrierEquiv_symm {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.dualCarrierEquiv = e.dualCarrierEquiv.symm

The dual-carrier restriction of an inverse isometry is the inverse equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.dualCarrierEquiv_trans {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} {U : Type w} [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).dualCarrierEquiv = e.dualCarrierEquiv ≪≫ₗ f.dualCarrierEquiv

The dual-carrier restriction of a composed isometry is the composite equivalence.