The spinor glue lattice D₈⁺ is the E₈ root lattice

The lattice D₈⁺ = D₈ ∪ (s + D₈) built by gluing the rank-eight checkerboard lattice along its spinor class is even and unimodular. This file proves the sharper statement that it is the root lattice of type E₈, by exhibiting an explicit isometry

E₈ ≃ D₈⁺.

The isometry is the rational linear map carrying the i-th standard coordinate vector of the simple-root model of E₈ to the i-th vector of Bourbaki's plate VII, written in the Conway--Sloane coordinates of D₈:

α₁ = (e₁ - e₂ - e₃ - e₄ - e₅ - e₆ - e₇ + e₈) / 2,
α₂ = e₁ + e₂,   α₃ = e₂ - e₁,   α₄ = e₃ - e₂,   α₅ = e₄ - e₃,
α₆ = e₅ - e₄,   α₇ = e₆ - e₅,   α₈ = e₇ - e₆.

Only α₁ leaves the checkerboard lattice, and it does so by exactly the Conway--Sloane spinor vector s = (e₁ + ⋯ + e₈) / 2, so all eight vectors lie in D₈⁺.

Three facts turn that list into an isometry of integral lattices.

• Their Gram matrix for the standard dot product is CartanMatrix.E 8. This is checked from doubled integer coordinates, so the verification is a decidable statement about integer matrices.
• The associated linear map is injective, because the E₈ form is nondegenerate and the map intertwines the two forms; an injective endomorphism of ℚ⁸ is bijective.
• Its image is the whole of D₈⁺. One inclusion is the membership check above. For the other, a vector x ∈ D₈⁺ has a rational preimage u, and ⟨u, v⟩_{E₈} = ⟨x, Φ v⟩ is an integer for every v in the E₈ carrier because D₈⁺ is integral; so u lies in the dual of the E₈ root lattice, which is the E₈ root lattice itself.

The last step is where unimodularity of E₈ enters, and it is what makes the inclusion an equality without any determinant computation. In particular the conclusion is a genuine lattice isometry and not the invalid inference that two even unimodular rank-eight lattices must be isometric.

Being an isometry, it transports every invariant: D₈⁺ inherits the E₈ root system's determinant 1 and trivial discriminant group. The resulting cardinality agrees with what the general overlattice comparison A_{L_H} ≅ H⊥ / H predicts for the order-two spinor glue subgroup H.

Main declarations

• TauCeti.IntegralLattice.e8GlueRoot: the eight Bourbaki simple roots of E₈, in the coordinates of the Conway--Sloane model of D₈, read off the library's shared integral table TauCeti.DynkinType.e8DoubledSimpleRoot.
• TauCeti.IntegralLattice.form_e8GlueRoot_e8GlueRoot: their Gram matrix is CartanMatrix.E 8.
• TauCeti.IntegralLattice.e8GlueRoot_mem_d8PlusCarrier: they lie in D₈⁺.
• TauCeti.IntegralLattice.span_range_e8GlueRoot: they span D₈⁺ over ℤ.
• TauCeti.IntegralLattice.e8GlueMap: the rational comparison map.
• TauCeti.IntegralLattice.typeE₈IsometryD8Plus: the isometry E₈ ≃ D₈⁺, whose inverse typeE₈IsometryD8Plus.symm is the isometry D₈⁺ ≃ E₈.
• TauCeti.IntegralLattice.d8PlusDiscriminantQuadraticIsometry: the discriminant quadratic form of D₈⁺ is that of E₈.
• TauCeti.IntegralLattice.natCard_orthogonalQuotient_d8SpinorSubgroup: the general comparison gives H⊥ / H cardinality one, as predicted by the direct E₈ computation.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, plate VII.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, §4.8.1.
• W. Ebeling, Lattices and Codes, Chapter 3.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 5, the D₈ ⊂ E₈ glue calculation.

The Bourbaki simple roots in Conway--Sloane coordinates

def TauCeti.IntegralLattice.e8GlueRoot (i : Fin 8) : Fin 8 → ℚ

The i-th simple root of E₈ in Bourbaki's numbering, written in the standard coordinates of the Conway--Sloane model of D₈.

The coordinates are read off the library's shared integral table TauCeti.DynkinType.e8DoubledSimpleRoot, whose row i is 2αᵢ₊₁ in exactly these coordinates. The doubling there clears the halves in α₁, so that every check on these vectors reduces to a decidable statement about integers.

Equations

• TauCeti.IntegralLattice.e8GlueRoot i j = ↑(TauCeti.DynkinType.e8DoubledSimpleRoot i j) / 2

@[simp]

theorem TauCeti.IntegralLattice.e8GlueRoot_apply (i j : Fin 8) : e8GlueRoot i j = ↑(DynkinType.e8DoubledSimpleRoot i j) / 2

The coordinates of a glue root are half the corresponding doubled integer coordinates.

The Gram matrix

theorem TauCeti.IntegralLattice.form_e8GlueRoot_e8GlueRoot (i j : Fin 8) : ((checkerboardLattice 8).form (e8GlueRoot i)) (e8GlueRoot j) = ↑(CartanMatrix.E 8 i j)

The Gram matrix of the eight glue roots is the Cartan matrix of type E₈.

Membership in the glue lattice

theorem TauCeti.IntegralLattice.e8GlueRoot_mem_d8PlusCarrier (i : Fin 8) : e8GlueRoot i ∈ ↑d8PlusCarrier

Every glue root lies in D₈⁺: the first differs from the spinor vector by a checkerboard vector, and the other seven are checkerboard vectors.

The comparison map

noncomputable def TauCeti.IntegralLattice.e8GlueMap : (Fin 8 → ℚ) →ₗ[ℚ] Fin 8 → ℚ

The rational linear map sending the i-th simple root of the E₈ root lattice to the i-th glue root of D₈⁺.

Equations

• TauCeti.IntegralLattice.e8GlueMap = ((Pi.basisFun ℚ (Fin 8)).constr ℚ) TauCeti.IntegralLattice.e8GlueRoot

@[simp]

theorem TauCeti.IntegralLattice.e8GlueMap_typeE₈SimpleRoot (i : Fin 8) : e8GlueMap (typeE₈SimpleRoot i) = e8GlueRoot i

The comparison map sends the i-th simple root of E₈ to the i-th glue root.

theorem TauCeti.IntegralLattice.form_comp_e8GlueMap : (checkerboardLattice 8).form.comp e8GlueMap e8GlueMap = typeE₈RootLattice.form

The comparison map intertwines the two forms: the standard dot product pulled back along it is the E₈ form.

theorem TauCeti.IntegralLattice.form_e8GlueMap (x y : Fin 8 → ℚ) : ((checkerboardLattice 8).form (e8GlueMap x)) (e8GlueMap y) = (typeE₈RootLattice.form x) y

The comparison map carries the E₈ form to the standard dot product.

The image of the E₈ carrier

theorem TauCeti.IntegralLattice.span_range_e8GlueRoot : Submodule.span ℤ (Set.range e8GlueRoot) = ↑d8PlusCarrier

The glue roots span D₈⁺ over ℤ.

One inclusion is the membership of each root. For the other, the preimage of a vector of D₈⁺ pairs integrally with the whole E₈ carrier, because D₈⁺ is an integral lattice containing the image of that carrier; so the preimage lies in the dual of the E₈ root lattice, which by unimodularity is the E₈ root lattice itself.

The isometry

noncomputable def TauCeti.IntegralLattice.typeE₈IsometryD8Plus : typeE₈RootLattice.Isometry d8PlusLattice

The E₈ root lattice is isometric to the spinor glue lattice D₈⁺.

The underlying rational equivalence sends the i-th simple root of E₈ to the i-th vector of Bourbaki's plate VII in Conway--Sloane coordinates.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈IsometryD8Plus_apply (x : Fin 8 → ℚ) : typeE₈IsometryD8Plus x = e8GlueMap x

theorem TauCeti.IntegralLattice.typeE₈IsometryD8Plus_typeE₈SimpleRoot (i : Fin 8) : typeE₈IsometryD8Plus (typeE₈SimpleRoot i) = e8GlueRoot i

The isometry sends the i-th E₈ simple root to the i-th glue root.

Cardinality from the general overlattice comparison

noncomputable def TauCeti.IntegralLattice.d8PlusDiscriminantQuadraticIsometry : (d8PlusLattice.discriminantQuadraticModule isEven_d8PlusLattice).Isometry (typeE₈RootLattice.discriminantQuadraticModule isEven_typeE₈RootLattice)

The discriminant quadratic form of D₈⁺ is the discriminant quadratic form of E₈.

The isometry is all that this declaration states. That the target is in turn the trivial form on a trivial group is recorded separately, by instSubsingletonDiscriminantGroupTypeE₈RootLattice and discriminantQuadraticMap_typeE₈RootLattice.

Equations

• TauCeti.IntegralLattice.d8PlusDiscriminantQuadraticIsometry = TauCeti.IntegralLattice.typeE₈IsometryD8Plus.symm.discriminantQuadraticIsometry TauCeti.IntegralLattice.isEven_d8PlusLattice

theorem TauCeti.IntegralLattice.natCard_orthogonalQuotient_d8SpinorSubgroup : Nat.card (((checkerboardLattice 8).discriminantQuadraticModule ⋯).orthogonalQuotient d8SpinorSubgroup isIsotropic_d8SpinorSubgroup).carrier = 1

The orthogonal quotient has the cardinality predicted by the direct E₈ computation.

Nikulin's comparison identifies the discriminant group of the glued lattice D₈⁺ with H⊥ / H for the order-two spinor glue subgroup H; the isometry above identifies it with the discriminant group of E₈. This theorem records the resulting cardinality of H⊥ / H.