Quotienting an integral lattice by its radical

The rational bilinear form of a possibly degenerate integral lattice descends to the quotient of its ambient space by its radical. The image of the integral carrier is again a full integral lattice, and the descended form is nondegenerate. This lets later discriminant-group constructions, which require nondegeneracy, be applied after discarding exactly the null directions.

The quotient map preserves the rational and integral forms. Evenness descends, and the quotient has signature (n₊, 0, n₋): its positive and negative indices agree with those of the original lattice, while its null index vanishes.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 1.
• TauCetiRoadmap/IntegralLattices/Suggested.lean.

Main definitions and results

• TauCeti.IntegralLattice.radicalQuotientForm: the descended rational bilinear form.
• TauCeti.IntegralLattice.radicalQuotientForm_mk: evaluation of the descended form on classes.
• TauCeti.IntegralLattice.radicalQuotientCarrier: the image of the integral carrier.
• TauCeti.IntegralLattice.mem_radicalQuotientCarrier_iff: representatives of carrier elements.
• TauCeti.IntegralLattice.radicalQuotient: the image lattice in the quotient ambient space.
• TauCeti.IntegralLattice.radicalQuotientMap: the quotient map on integral carriers.
• TauCeti.IntegralLattice.radicalQuotientMap_surjective: the quotient map on carriers is surjective.
• TauCeti.IntegralLattice.radicalQuotientMap_eq_zero_iff: the map discards exactly the radical.
• TauCeti.IntegralLattice.form_radicalQuotientMap: preservation of the rational form.
• TauCeti.IntegralLattice.integralForm_radicalQuotientMap: preservation of the integral form.
• TauCeti.IntegralLattice.radicalQuotient_norm_mk: preservation of the rational norm.
• TauCeti.IntegralLattice.integralNorm_radicalQuotientMap: preservation of the integral norm.
• TauCeti.IntegralLattice.nondegenerate_radicalQuotientForm: the descended form is nondegenerate.
• TauCeti.IntegralLattice.nondegenerate_radicalQuotient: the bilinear form of the radical quotient is nondegenerate.
• TauCeti.IntegralLattice.radical_radicalQuotient_eq_bot: the quotient radical is trivial.
• TauCeti.IntegralLattice.IsEven.radicalQuotient: evenness descends to the quotient.
• TauCeti.IntegralLattice.sigPos_radicalQuotient: preservation of the positive index.
• TauCeti.IntegralLattice.sigNeg_radicalQuotient: preservation of the negative index.
• TauCeti.IntegralLattice.signature_radicalQuotient: the quotient signature is (n₊, 0, n₋).

noncomputable def TauCeti.IntegralLattice.radicalQuotientForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : LinearMap.BilinForm ℚ (V ⧸ L.radical)

The bilinear form induced on the quotient of the ambient space by the lattice radical.

Equations

• L.radicalQuotientForm = QuadraticMap.associated ((LinearMap.BilinMap.toQuadraticMap L.form).lift L.radical ⋯)

@[simp]

theorem TauCeti.IntegralLattice.radicalQuotientForm_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : V) : (L.radicalQuotientForm (Submodule.Quotient.mk x)) (Submodule.Quotient.mk y) = (L.form x) y

The quotient form evaluated on classes is the original form evaluated on representatives.

theorem TauCeti.IntegralLattice.isSymm_radicalQuotientForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotientForm.IsSymm

The form induced on the radical quotient is symmetric.

def TauCeti.IntegralLattice.radicalQuotientCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule ℤ (V ⧸ L.radical)

The image of the integral carrier in the quotient by the radical.

Equations

• L.radicalQuotientCarrier = Submodule.map (↑ℤ L.radical.mkQ) L.carrier

@[simp]

theorem TauCeti.IntegralLattice.mem_radicalQuotientCarrier_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V ⧸ L.radical) : x ∈ L.radicalQuotientCarrier ↔ ∃ y ∈ L.carrier, Submodule.Quotient.mk y = x

A quotient class belongs to the quotient carrier exactly when it has a representative in the original integral carrier.

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

The image of a full integral carrier in the radical quotient is again a full lattice.

noncomputable def TauCeti.IntegralLattice.radicalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : IntegralLattice (V ⧸ L.radical)

The radical quotient of an integral lattice. Its carrier is the image of the original carrier, and its form is the form induced on the quotient ambient space.

Equations

• L.radicalQuotient = TauCeti.IntegralLattice.ofSubmodule L.radicalQuotientCarrier L.radicalQuotientForm ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.radicalQuotient_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.carrier = L.radicalQuotientCarrier

@[simp]

theorem TauCeti.IntegralLattice.radicalQuotient_form {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.form = L.radicalQuotientForm

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

The quotient map from the original integral carrier to the radical-quotient carrier.

Equations

• L.radicalQuotientMap = LinearMap.codRestrict L.radicalQuotient.carrier ((↑ℤ L.radical.mkQ).domRestrict L.carrier) ⋯

@[simp]

theorem TauCeti.IntegralLattice.radicalQuotientMap_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) : ↑(L.radicalQuotientMap x) = Submodule.Quotient.mk ↑x

Evaluation rule for the radical quotient map.

theorem TauCeti.IntegralLattice.radicalQuotientMap_surjective {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Function.Surjective ⇑L.radicalQuotientMap

The radical quotient map on integral lattices is surjective.

@[simp]

theorem TauCeti.IntegralLattice.radicalQuotientMap_eq_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) : L.radicalQuotientMap x = 0 ↔ ↑x ∈ L.radical

A lattice vector maps to zero exactly when its ambient vector belongs to the radical.

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

The radical quotient map preserves the rational bilinear form.

@[simp]

theorem TauCeti.IntegralLattice.integralForm_radicalQuotientMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) : (L.radicalQuotient.integralForm (L.radicalQuotientMap x)) (L.radicalQuotientMap y) = (L.integralForm x) y

The radical quotient map preserves the integral bilinear form.

@[simp]

theorem TauCeti.IntegralLattice.radicalQuotient_norm_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V) : L.radicalQuotient.norm (Submodule.Quotient.mk x) = L.norm x

The radical quotient preserves the rational norm on representatives.

@[simp]

theorem TauCeti.IntegralLattice.integralNorm_radicalQuotientMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) : L.radicalQuotient.integralNorm (L.radicalQuotientMap x) = L.integralNorm x

The radical quotient map preserves the integral norm.

theorem TauCeti.IntegralLattice.nondegenerate_radicalQuotientForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotientForm.Nondegenerate

The form on the radical quotient is nondegenerate.

theorem TauCeti.IntegralLattice.nondegenerate_radicalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.form.Nondegenerate

The bilinear form of the radical quotient is nondegenerate.

@[simp]

theorem TauCeti.IntegralLattice.radical_radicalQuotient_eq_bot {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.radical = ⊥

The radical of the quotient lattice is trivial.

theorem TauCeti.IntegralLattice.IsEven.radicalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) : L.radicalQuotient.IsEven

Evenness passes from an integral lattice to its radical quotient.

@[simp]

theorem TauCeti.IntegralLattice.sigPos_radicalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.sigPos = L.sigPos

The positive index is unchanged after quotienting by the radical.

@[simp]

theorem TauCeti.IntegralLattice.sigNeg_radicalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.sigNeg = L.sigNeg

The negative index is unchanged after quotienting by the radical.

@[simp]

theorem TauCeti.IntegralLattice.signature_radicalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radicalQuotient.signature = (L.sigPos, 0, L.sigNeg)

The radical quotient has the same positive and negative indices as the original lattice and zero null index.