Discriminant groups of integral lattices

For a nondegenerate integral lattice L, its discriminant group is the finite quotient

A_L = Lᵛ / L.

Both lattices in this expression are submodules of the same rational ambient vector space. To form the quotient, carrierInDual realizes L.carrier as a submodule of the subtype L.dualCarrier. The quotient is defined without a nondegeneracy hypothesis, while its finiteness uses nondegeneracy through the fact that the dual carrier is a full lattice of the same rank.

An isometry of integral lattices restricts to an equivalence of dual carriers and hence induces an equivalence of discriminant groups. The construction respects identity, inverse, and composition.

Main declarations

• TauCeti.IntegralLattice.carrierInDual: the original carrier inside its dual carrier.
• TauCeti.IntegralLattice.carrierInDualBasis: a carrier basis, regarded as a basis of its copy inside the dual carrier.
• TauCeti.IntegralLattice.DiscriminantGroup: the quotient Lᵛ / L.
• TauCeti.IntegralLattice.instFiniteDiscriminantGroup: finiteness in the nondegenerate case.
• TauCeti.IntegralLattice.finite_discriminantGroup_iff_nondegenerate: finiteness holds exactly in the nondegenerate case.
• TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv: the induced equivalence of discriminant groups.

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.

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

The original carrier, regarded as a submodule of the subtype L.dualCarrier.

Equations

• L.carrierInDual = L.carrier.submoduleOf L.dualCarrier

@[simp]

theorem TauCeti.IntegralLattice.mem_carrierInDual_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.dualCarrier) : x ∈ L.carrierInDual ↔ ↑x ∈ L.carrier

Membership in carrierInDual is membership of the underlying ambient vector in the original carrier.

theorem TauCeti.IntegralLattice.carrierInDual_eq_submoduleOf {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.carrierInDual = L.carrier.submoduleOf L.dualCarrier

The embedded carrier is the copy of the ambient carrier inside the dual carrier.

@[simp]

theorem TauCeti.IntegralLattice.map_carrierInDual_subtype {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.map L.dualCarrier.subtype L.carrierInDual = L.carrier

Mapping the embedded carrier back into the ambient space recovers the original carrier.

theorem TauCeti.IntegralLattice.finrank_carrierInDual {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Module.finrank ℤ ↥L.carrierInDual = Module.finrank ℤ ↥L.carrier

The copy of the carrier inside the dual carrier has the same rank as the carrier.

noncomputable def TauCeti.IntegralLattice.carrierInDualBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (b : Module.Basis ι ℤ ↥L.carrier) : Module.Basis ι ℤ ↥L.carrierInDual

A basis of the carrier, regarded as a basis of its copy inside the dual carrier.

Equations

• L.carrierInDualBasis b = b.map (Submodule.submoduleOfEquivOfLe ⋯).symm

@[simp]

theorem TauCeti.IntegralLattice.coe_carrierInDualBasis_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (b : Module.Basis ι ℤ ↥L.carrier) (i : ι) : ↑((L.carrierInDualBasis b) i) = ⟨↑(b i), ⋯⟩

The vector of carrierInDualBasis indexed by i has underlying carrier vector b i.

@[reducible, inline]

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

The discriminant group A_L = Lᵛ / L, as an actual quotient of the dual-carrier subtype by the inverse image of the original carrier.

Equations

• L.DiscriminantGroup = (↥L.dualCarrier ⧸ L.carrierInDual)

theorem TauCeti.IntegralLattice.discriminantGroup_mk_eq_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.dualCarrier) : Submodule.Quotient.mk x = 0 ↔ ↑x ∈ L.carrier

A representative defines the zero discriminant class exactly when its ambient vector belongs to the original carrier.

@[simp]

theorem TauCeti.IntegralLattice.discriminantGroup_mk_eq_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.dualCarrier) : Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ ↑(x - y) ∈ L.carrier

Two representatives define the same discriminant class exactly when their difference belongs to the original carrier.

instance TauCeti.IntegralLattice.instFiniteDiscriminantGroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : Finite L.DiscriminantGroup

The discriminant group of a nondegenerate integral lattice is finite.

theorem TauCeti.IntegralLattice.finite_discriminantGroup_iff_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Finite L.DiscriminantGroup ↔ L.form.Nondegenerate

The discriminant group is finite exactly when the lattice form is nondegenerate.

theorem TauCeti.IntegralLattice.Isometry.map_carrierInDual {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.dualCarrierEquiv) L.carrierInDual = M.carrierInDual

The dual-carrier equivalence maps the embedded original carrier onto the embedded target carrier.

def TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv {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.DiscriminantGroup ≃ₗ[ℤ] M.DiscriminantGroup

An integral-lattice isometry induces a linear equivalence of discriminant groups.

Equations

• e.discriminantGroupEquiv = Submodule.Quotient.equiv L.carrierInDual M.carrierInDual e.dualCarrierEquiv ⋯

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_mk {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.discriminantGroupEquiv (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e.dualCarrierEquiv x)

The induced discriminant-group equivalence maps the class of a representative to the class of its image.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).discriminantGroupEquiv = LinearEquiv.refl ℤ L.DiscriminantGroup

The identity isometry induces the identity equivalence of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_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.discriminantGroupEquiv = e.discriminantGroupEquiv.symm

The equivalence induced by an inverse isometry is the inverse of the induced equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_symm_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (y : ↥M.dualCarrier) : e.discriminantGroupEquiv.symm (Submodule.Quotient.mk y) = Submodule.Quotient.mk (e.symm.dualCarrierEquiv y)

The inverse induced discriminant-group equivalence maps a representative through the inverse dual-carrier equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_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).discriminantGroupEquiv = e.discriminantGroupEquiv ≪≫ₗ f.discriminantGroupEquiv

The equivalence induced by a composite isometry is the composite of the induced equivalences.