The even sublattice of an integral lattice

The kernel of norm parity consists exactly of the vectors with even integral norm. It contains twice the carrier, so its image in the original rational ambient space is full. Restricting the form gives a canonical even sublattice with the same signature. For an odd lattice the quotient by this submodule is canonically ℤ/2 through norm parity.

The even sublattice supplies the discriminant-form construction used to prove van der Blij's characteristic-norm congruence for odd unimodular lattices.

References

• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.

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

The submodule of lattice vectors with even integral norm, defined as the norm-parity kernel.

@[simp]

theorem TauCeti.IntegralLattice.mem_evenSubmodule_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) : x ∈ L.evenSubmodule ↔ Even (L.integralNorm x)

Membership in the norm-parity kernel means that the integral norm is even.

theorem TauCeti.IntegralLattice.two_smul_mem_evenSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) : 2 • x ∈ L.evenSubmodule

Twice every lattice vector lies in the even-norm submodule.

instance TauCeti.IntegralLattice.instIsLatticeEvenSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.IsLattice ℚ (Submodule.map L.carrier.subtype L.evenSubmodule)

The embedded even-norm submodule is full: it contains the full sublattice 2L.

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

The canonical even sublattice in the original rational ambient space.

@[simp]

theorem TauCeti.IntegralLattice.evenSublattice_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.evenSublattice.carrier = Submodule.map L.carrier.subtype L.evenSubmodule

The even sublattice's carrier is the embedded norm-parity kernel.

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

The even sublattice is contained in the original lattice carrier.

theorem TauCeti.IntegralLattice.evenSublattice_carrier_submoduleOf {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.evenSublattice.carrier.submoduleOf L.carrier = L.evenSubmodule

Viewed in the original carrier, the even sublattice is exactly the norm-parity kernel.

theorem TauCeti.IntegralLattice.mem_evenSublattice_carrier_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) : ↑x ∈ L.evenSublattice.carrier ↔ Even (L.integralNorm x)

A vector of the original lattice belongs to the even sublattice exactly when its norm is even.

@[simp]

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

The even sublattice retains the original rational bilinear form.

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

Every vector of the even sublattice has even integral norm.

instance TauCeti.IntegralLattice.instIsNondegenerateEvenSublattice {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : L.evenSublattice.IsNondegenerate

The even sublattice is nondegenerate whenever the original lattice is nondegenerate.

@[simp]

theorem TauCeti.IntegralLattice.evenSublattice_signature {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.evenSublattice.signature = L.signature

Passing to the full even sublattice preserves all three signature indices.

instance TauCeti.IntegralLattice.instFiniteQuotientEvenSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Finite (↥L.carrier ⧸ L.evenSubmodule)

The norm-parity kernel has finite quotient, through the finite range in ℤ/2.

theorem TauCeti.IntegralLattice.normParity_surjective_of_not_isEven {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : ¬L.IsEven) : Function.Surjective ⇑L.normParity

Norm parity is surjective when the lattice is not even.

noncomputable def TauCeti.IntegralLattice.evenSubmoduleQuotientEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : ¬L.IsEven) : (↥L.carrier ⧸ L.evenSubmodule) ≃ₗ[ℤ] ZMod 2

For an odd lattice, norm parity identifies the quotient by the even submodule with ℤ/2.

@[simp]

theorem TauCeti.IntegralLattice.evenSubmoduleQuotientEquiv_apply_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : ¬L.IsEven) (x : ↥L.carrier) : (L.evenSubmoduleQuotientEquiv hL) (Submodule.Quotient.mk x) = L.normParity x

The quotient equivalence evaluates a lattice-vector class by its norm parity.

theorem TauCeti.IntegralLattice.natCard_quotient_evenSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : ¬L.IsEven) : Nat.card (↥L.carrier ⧸ L.evenSubmodule) = 2

The even submodule has index two in every odd integral lattice.

theorem TauCeti.IntegralLattice.relIndex_evenSublattice_le_two {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.evenSublattice.carrier.toAddSubgroup.relIndex L.carrier.toAddSubgroup ≤ 2

The even sublattice has index at most two in the lattice: it is the kernel of norm parity.