Finiteness of dual integral lattices

The dual carrier of an integral lattice always spans the ambient rational vector space: it contains the original full carrier. Its finite generation is subtler. It is finitely generated over ℤ, and hence a full lattice, exactly when the ambient bilinear form is nondegenerate.

The converse is the load-bearing direction. Every vector in the left radical, together with all of its rational multiples, lies in the dual carrier. If that carrier were finitely generated, a coordinate of such a vector in an integral basis would be divisible by every prime and therefore zero. Applying this to every coordinate forces the radical vector itself to vanish. Symmetry then gives nondegeneracy on both sides.

Main results

• TauCeti.IntegralLattice.span_dualCarrier_eq_top: the dual carrier always spans the ambient rational vector space.
• TauCeti.IntegralLattice.moduleFinite_dualCarrier_iff_nondegenerate: the dual carrier is a finite ℤ-module exactly when the form is nondegenerate.
• TauCeti.IntegralLattice.fg_dualCarrier_iff_nondegenerate: the equivalent finite-generation formulation.
• TauCeti.IntegralLattice.isLattice_dualCarrier_iff_nondegenerate: the dual carrier is a full lattice exactly when the form is nondegenerate.

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.

theorem TauCeti.IntegralLattice.span_dualCarrier_eq_top {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.span ℚ ↑L.dualCarrier = ⊤

The dual carrier always spans the rational ambient space, without a nondegeneracy hypothesis.

theorem TauCeti.IntegralLattice.smul_mem_dualCarrier_of_mem_ker {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {x : V} (hx : x ∈ LinearMap.ker L.form) (a : ℚ) : a • x ∈ L.dualCarrier

Every rational multiple of a vector in the left radical belongs to the dual carrier.

theorem TauCeti.IntegralLattice.nondegenerate_of_moduleFinite_dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [Module.Finite ℤ ↥L.dualCarrier] : L.form.Nondegenerate

If the dual carrier is finite as a ℤ-module, then the lattice form is nondegenerate.

theorem TauCeti.IntegralLattice.moduleFinite_dualCarrier_iff_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Module.Finite ℤ ↥L.dualCarrier ↔ L.form.Nondegenerate

The dual carrier is finite as a ℤ-module exactly when the lattice form is nondegenerate.

theorem TauCeti.IntegralLattice.fg_dualCarrier_iff_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.dualCarrier.FG ↔ L.form.Nondegenerate

The dual carrier is finitely generated over ℤ exactly when the lattice form is nondegenerate.

theorem TauCeti.IntegralLattice.isLattice_dualCarrier_iff_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.IsLattice ℚ L.dualCarrier ↔ L.form.Nondegenerate

The dual carrier is a full integral lattice exactly when the lattice form is nondegenerate.