The spinor glue enlargement of the checkerboard lattice in rank eight

This file constructs the lattice D₈⁺ by gluing the rank-eight checkerboard lattice along its spinor class. The gluing subgroup is the cyclic subgroup generated by the Conway--Sloane spinor class in the discriminant group of D₈. Its inverse image is identified literally as

D₈⁺ = D₈ ∪ (s + D₈),

where s = (1/2, ..., 1/2). The spinor class has order two and quadratic value zero, so the inverse image is an even lattice of index two. The overlattice discriminant formula then shows that D₈⁺ has discriminant one and is unimodular.

The subsequent identification of this coordinate lattice with the positive E₈ root lattice requires the exceptional-root-lattice bridge and is deliberately separate. The definitions here use the same spinor representative as the type D discriminant-form calculation, so that bridge does not need a change of coordinates.

Main declarations

• TauCeti.IntegralLattice.d8SpinorSubgroup: the order-two subgroup generated by the spinor class in A_{D₈}.
• TauCeti.IntegralLattice.d8PlusCarrier: its inverse image in the dual of D₈.
• TauCeti.IntegralLattice.mem_d8PlusCarrier_iff: the formula D₈⁺ = D₈ ∪ (s + D₈).
• TauCeti.IntegralLattice.d8PlusLattice: the resulting even integral lattice.
• TauCeti.IntegralLattice.toIntegralLattice_eq_d8PlusLattice: the general glued-overlattice construction along the spinor subgroup is d8PlusLattice.
• TauCeti.IntegralLattice.isUnimodular_d8PlusLattice: D₈⁺ is unimodular.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, §4.8.1.
• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4, Proposition 1.4.1.
• W. Ebeling, Lattices and Codes, Chapter 3.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 5, the D₈ ⊂ E₈ glue calculation.
• TauCetiRoadmap/IntegralLattices/Suggested.lean (d8SpinorSubgroup, natCard_d8SpinorSubgroup, d8Plus, d8Plus_isUnimodular).

noncomputable def TauCeti.IntegralLattice.d8SpinorSubgroup : AddSubgroup (checkerboardLattice 8).DiscriminantGroup

The glue subgroup of A_{D₈} generated by the Conway--Sloane spinor class.

Equations

• TauCeti.IntegralLattice.d8SpinorSubgroup = AddSubgroup.zmultiples (TauCeti.IntegralLattice.checkerboardSpinorClass 8)

@[simp]

theorem TauCeti.IntegralLattice.mem_d8SpinorSubgroup_iff (x : (checkerboardLattice 8).DiscriminantGroup) : x ∈ d8SpinorSubgroup ↔ x = 0 ∨ x = checkerboardSpinorClass 8

A discriminant class belongs to the spinor glue subgroup exactly when it is zero or the spinor class.

theorem TauCeti.IntegralLattice.natCard_d8SpinorSubgroup : Nat.card ↥d8SpinorSubgroup = 2

The spinor glue subgroup has order two.

noncomputable def TauCeti.IntegralLattice.d8PlusCarrier : ↑(checkerboardLattice 8).IntermediateCarrier

The intermediate carrier obtained by gluing D₈ along its spinor class.

Equations

• TauCeti.IntegralLattice.d8PlusCarrier = (TauCeti.IntegralLattice.checkerboardLattice 8).intermediateCarrierOfDiscriminantSubgroup TauCeti.IntegralLattice.d8SpinorSubgroup

@[simp]

theorem TauCeti.IntegralLattice.mem_d8PlusCarrier_iff (x : Fin 8 → ℚ) : x ∈ ↑d8PlusCarrier ↔ x ∈ (checkerboardLattice 8).carrier ∨ x - checkerboardSpinor 8 ∈ (checkerboardLattice 8).carrier

A vector belongs to D₈⁺ exactly when it belongs to D₈, or differs from the spinor vector by an element of D₈. This is the literal coordinate formula D₈⁺ = D₈ ∪ (s + D₈).

@[simp]

theorem TauCeti.IntegralLattice.discriminantSubgroup_d8PlusCarrier : (checkerboardLattice 8).discriminantSubgroup d8PlusCarrier = d8SpinorSubgroup

The discriminant subgroup cut out by d8PlusCarrier is the spinor glue subgroup.

theorem TauCeti.IntegralLattice.d8SpinorClass_quadratic_eq_zero : ((checkerboardLattice 8).discriminantQuadraticMap ⋯) (checkerboardSpinorClass 8) = 0

The rank-eight spinor class has quadratic value zero.

theorem TauCeti.IntegralLattice.isIsotropic_d8SpinorSubgroup : ((checkerboardLattice 8).discriminantQuadraticModule ⋯).IsIsotropic d8SpinorSubgroup

The spinor glue subgroup is quadratic-isotropic.

theorem TauCeti.IntegralLattice.isEven_d8PlusCarrier : IntermediateCarrier.IsEven d8PlusCarrier

The spinor glue carrier is even: its only nonzero glue class has quadratic value 8 / 8 = 0 in ℚ/ℤ.

noncomputable def TauCeti.IntegralLattice.d8PlusLattice : IntegralLattice (Fin 8 → ℚ)

The D₈⁺ integral lattice, obtained from the even spinor glue carrier with the same standard dot product as the checkerboard lattice.

Equations

• TauCeti.IntegralLattice.d8PlusLattice = TauCeti.IntegralLattice.d8PlusLattice._proof_3✝.toIntegralLattice

theorem TauCeti.IntegralLattice.toIntegralLattice_eq_d8PlusLattice (h : IntermediateCarrier.IsEven ((checkerboardLattice 8).intermediateCarrierOfDiscriminantSubgroup d8SpinorSubgroup)) : ⋯.toIntegralLattice = d8PlusLattice

The even overlattice glued along the spinor subgroup is the D₈⁺ lattice. This exposes d8PlusLattice to the general overlattice theorems, which name the glued lattice through a proof of evenness of the inverse image.

@[simp]

theorem TauCeti.IntegralLattice.d8PlusLattice_carrier : d8PlusLattice.carrier = ↑d8PlusCarrier

The carrier of the D₈⁺ lattice is the spinor glue carrier.

@[simp]

theorem TauCeti.IntegralLattice.d8PlusLattice_form : d8PlusLattice.form = (checkerboardLattice 8).form

The form of D₈⁺ is the standard dot product inherited from D₈.

instance TauCeti.IntegralLattice.instIsNondegenerateD8PlusLattice : d8PlusLattice.IsNondegenerate

The D₈⁺ lattice is nondegenerate.

theorem TauCeti.IntegralLattice.isEven_d8PlusLattice : d8PlusLattice.IsEven

The D₈⁺ lattice is even.

theorem TauCeti.IntegralLattice.index_d8PlusCarrier : IntermediateCarrier.index d8PlusCarrier = 2

The spinor enlargement D₈ ⊂ D₈⁺ has index two.

theorem TauCeti.IntegralLattice.discriminant_d8PlusLattice : d8PlusLattice.discriminant = 1

The D₈⁺ lattice has discriminant one.

theorem TauCeti.IntegralLattice.isUnimodular_d8PlusLattice : d8PlusLattice.IsUnimodular

The spinor glue enlargement D₈⁺ is unimodular.