The Leech lattice from Construction B and an odd shift

Let K be the Construction B lattice of the extended binary Golay code: the integer vectors of ℚ^(Fin 24) reducing to a Golay codeword modulo two and having coordinate sum divisible by four, with the halved dot product B(x, y) = (∑ xᵢ yᵢ) / 2. It is even of discriminant four.

The odd Leech shift is s = (-3/2, 1/2, …, 1/2), the distinguished coordinate being 0. It pairs integrally with K, since B(s, x) = (∑ xᵢ) / 4 - x₀; it has norm B(s, s) = 4; and 2s = (-3, 1, …, 1) lies in K while s does not, because its coordinates are not integers. Its class therefore generates an order-two subgroup of the discriminant group A_K, which is quadratic-isotropic because B(s, s) / 2 is an integer, and Lagrangian because 2² = #A_K.

The Leech lattice is the even overlattice of K glued along this subgroup. Its carrier is literally K ∪ (s + K), and it is a positive definite, even, unimodular lattice of rank 24. Its congruence model and rootlessness, which use the Golay weights, are proved in TauCeti.LinearAlgebra.IntegralLattice.Rank24.Leech.Minimum.

Main declarations

• TauCeti.leechShift: the odd shift (-3/2, 1/2, …, 1/2).
• TauCeti.leechShiftClass, TauCeti.leechShiftSubgroup: its discriminant class and the order-two Lagrangian subgroup it generates.
• TauCeti.leechLattice: the Leech lattice, with the carrier decomposition TauCeti.mem_leechLattice_carrier_iff, and TauCeti.isEven_leechLattice, TauCeti.isUnimodular_leechLattice, TauCeti.isPosDef_leechLattice, and TauCeti.finrank_leechLattice.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §11, and Chapter 10.
• R. A. Wilson, The Finite Simple Groups, §5.4.

The odd shift

def TauCeti.leechShift : Fin 24 → ℚ

The odd Leech shift (-3/2, 1/2, …, 1/2), whose distinguished coordinate is 0.

@[simp]

theorem TauCeti.leechShift_zero : leechShift 0 = -(3 / 2)

The distinguished coordinate of the Leech shift is -3/2.

@[simp]

theorem TauCeti.leechShift_of_ne_zero {i : Fin 24} (hi : i ≠ 0) : leechShift i = 1 / 2

Every other coordinate of the Leech shift is 1/2.

theorem TauCeti.leechShift_ne_zero : leechShift ≠ 0

The Leech shift is nonzero.

theorem TauCeti.leechShift_dotProduct (x : Fin 24 → ℚ) : leechShift ⬝ᵥ x = (∑ i : Fin 24, x i) / 2 - 2 * x 0

The dot product with the Leech shift is half the coordinate sum minus twice the distinguished coordinate.

theorem TauCeti.constructionBLattice_form_leechShift_left (x : Fin 24 → ℚ) : (BinaryGolay.constructionBLattice.form leechShift) x = (∑ i : Fin 24, x i) / 4 - x 0

The Golay Construction B form pairs the Leech shift with x to a quarter of the coordinate sum minus the distinguished coordinate.

theorem TauCeti.constructionBLattice_form_leechShift_leechShift : (BinaryGolay.constructionBLattice.form leechShift) leechShift = 4

The Leech shift has norm four.

theorem TauCeti.leechShift_mem_constructionBLattice_dualCarrier : leechShift ∈ BinaryGolay.constructionBLattice.dualCarrier

The Leech shift pairs integrally with Construction B: for x in Construction B, B(s, x) = (∑ xᵢ) / 4 - x₀ is an integer.

theorem TauCeti.two_zsmul_leechShift_mem_constructionBLattice_carrier : 2 • leechShift ∈ BinaryGolay.constructionBLattice.carrier

Twice the Leech shift, (-3, 1, …, 1), lies in Construction B: it reduces to the all-ones Golay word and has coordinate sum 20.

theorem TauCeti.leechShift_notMem_constructionBLattice_carrier : leechShift ∉ BinaryGolay.constructionBLattice.carrier

The Leech shift does not lie in Construction B, whose vectors have integer coordinates.

The glue subgroup

noncomputable def TauCeti.leechShiftClass : BinaryGolay.constructionBLattice.DiscriminantGroup

The discriminant class of the Leech shift in the Golay Construction B lattice.

theorem TauCeti.leechShiftClass_def : leechShiftClass = Submodule.Quotient.mk ⟨leechShift, leechShift_mem_constructionBLattice_dualCarrier⟩

The class of the Leech shift is represented by the Leech shift.

theorem TauCeti.leechShiftClass_ne_zero : leechShiftClass ≠ 0

The class of the Leech shift is nonzero.

theorem TauCeti.two_nsmul_leechShiftClass : 2 • leechShiftClass = 0

Twice the class of the Leech shift vanishes.

@[simp]

theorem TauCeti.addOrderOf_leechShiftClass : addOrderOf leechShiftClass = 2

The class of the Leech shift has order two.

noncomputable def TauCeti.leechShiftSubgroup : AddSubgroup BinaryGolay.constructionBLattice.DiscriminantGroup

The Leech glue subgroup of the discriminant group of the Golay Construction B lattice, generated by the class of the Leech shift.

@[simp]

theorem TauCeti.mem_leechShiftSubgroup_iff (x : BinaryGolay.constructionBLattice.DiscriminantGroup) : x ∈ leechShiftSubgroup ↔ x = 0 ∨ x = leechShiftClass

The Leech glue subgroup consists of zero and the class of the Leech shift.

theorem TauCeti.natCard_leechShiftSubgroup : Nat.card ↥leechShiftSubgroup = 2

The Leech glue subgroup has order two.

@[simp]

theorem TauCeti.discriminantQuadraticMap_leechShiftClass : (BinaryGolay.constructionBLattice.discriminantQuadraticMap BinaryGolay.isEven_constructionBLattice) leechShiftClass = 0

The discriminant quadratic map vanishes on the class of the Leech shift, whose half-norm 4 / 2 is an integer.

theorem TauCeti.isIsotropic_leechShiftSubgroup : (BinaryGolay.constructionBLattice.discriminantQuadraticModule BinaryGolay.isEven_constructionBLattice).IsIsotropic leechShiftSubgroup

The Leech glue subgroup is quadratic-isotropic.

theorem TauCeti.isLagrangian_leechShiftSubgroup : (BinaryGolay.constructionBLattice.discriminantQuadraticModule BinaryGolay.isEven_constructionBLattice).IsLagrangian leechShiftSubgroup

The Leech glue subgroup is Lagrangian: it is isotropic of order two in a discriminant group of order four.

The Leech lattice

noncomputable def TauCeti.leechLattice : IntegralLattice (Fin 24 → ℚ)

The Leech lattice, glued from the Golay Construction B lattice along the order-two subgroup generated by the odd shift (-3/2, 1/2, …, 1/2). Its carrier is the union of the Construction B lattice and its translate by the shift, by mem_leechLattice_carrier_iff.

theorem TauCeti.leechLattice_carrier : leechLattice.carrier = ↑(BinaryGolay.constructionBLattice.intermediateCarrierOfDiscriminantSubgroup leechShiftSubgroup)

The carrier of the Leech lattice is the inverse image of the Leech glue subgroup.

@[simp]

theorem TauCeti.leechLattice_form : leechLattice.form = ConstructionA.form 2

The form of the Leech lattice is the halved coordinate dot product.

@[simp]

theorem TauCeti.mem_leechLattice_carrier_iff (x : Fin 24 → ℚ) : x ∈ leechLattice.carrier ↔ x ∈ BinaryGolay.constructionBLattice.carrier ∨ x - leechShift ∈ BinaryGolay.constructionBLattice.carrier

The carrier decomposition of the Leech lattice: a vector lies in the Leech lattice exactly when it or its difference with the odd shift lies in the Golay Construction B lattice.

theorem TauCeti.constructionBLattice_carrier_le_leechLattice_carrier : BinaryGolay.constructionBLattice.carrier ≤ leechLattice.carrier

The Golay Construction B lattice is a sublattice of the Leech lattice.

theorem TauCeti.leechShift_mem_leechLattice_carrier : leechShift ∈ leechLattice.carrier

The odd shift lies in the Leech lattice.

theorem TauCeti.relIndex_constructionBLattice_leechLattice : BinaryGolay.constructionBLattice.carrier.toAddSubgroup.relIndex leechLattice.carrier.toAddSubgroup = 2

The Golay Construction B lattice has index two in the Leech lattice.

instance TauCeti.instIsNondegenerateLeechLattice : leechLattice.IsNondegenerate

The Leech lattice is nondegenerate.

theorem TauCeti.isEven_leechLattice : leechLattice.IsEven

The Leech lattice is even.

theorem TauCeti.isUnimodular_leechLattice : leechLattice.IsUnimodular

The Leech lattice is unimodular, being glued along a Lagrangian subgroup.

@[simp]

theorem TauCeti.discriminant_leechLattice : leechLattice.discriminant = 1

The Leech lattice has discriminant one.

theorem TauCeti.isPosDef_leechLattice : leechLattice.IsPosDef

The Leech lattice is positive definite.

@[simp]

theorem TauCeti.finrank_leechLattice : Module.finrank ℤ ↥leechLattice.carrier = 24

The Leech lattice has rank 24.

theorem TauCeti.leechLattice_form_leechShift_leechShift : (leechLattice.form leechShift) leechShift = 4

The odd shift is a vector of norm four in the Leech lattice.