The exceptional root lattices E₆, E₇, E₈ and their discriminant forms

The root lattice of an exceptional simply laced type is the integral lattice whose Gram matrix in the simple-root basis is the corresponding Cartan matrix. This file constructs the three of them inside Fin n → ℚ, proves them even and nondegenerate, and computes their discriminant forms:

det E₆ = 3,   A_{E₆} ≃+ ℤ/3,   q(ϖ₁) = 2/3,
det E₇ = 2,   A_{E₇} ≃+ ℤ/2,   q(ϖ₇) = 3/4,
det E₈ = 1,   A_{E₈} = 0,      E₈ is unimodular.

Their levels are respectively 3, 4, and 1, computed from these quadratic values using IntegralLattice.IsEven.level_eq_den and the even-unimodular criterion.

The generators are the classes of the minuscule fundamental weights, ϖ₁ for E₆ and ϖ₇ for E₇, written in the simple-root coordinates that the inverse Cartan matrix dictates:

3 ϖ₁ = 4α₁ + 3α₂ + 5α₃ + 6α₄ + 4α₅ + 2α₆,
2 ϖ₇ = 2α₁ + 3α₂ + 4α₃ + 6α₄ + 5α₅ + 4α₆ + 3α₇.

Those coordinates are verified against the lattice rather than assumed: form_typeE₆MinusculeWeight_typeE₆SimpleRoot proves ⟨ϖ₁, αᵢ⟩ = δ_{i,1} directly from the row combinations of CartanMatrix.E 6, and likewise in type E₇. The self-pairings ⟨ϖ₁, ϖ₁⟩ = 4/3 and ⟨ϖ₇, ϖ₇⟩ = 3/2 follow, and give the displayed half-norm values. The class of ϖ₁ has additive order exactly 3 because the first simple-root coordinate of ϖ₁ is 4/3, and the discriminant group has that same order, so ϖ₁ generates; the same argument with the second coordinate 3/2 of ϖ₇ and the order 2 settles type E₇.

The half-norm convention is q_L(x) = ⟨x,x⟩ / 2 in ℚ/ℤ. Nikulin's full-norm values for these rows are 4/3 and 3/2.

Both cyclic discriminant forms are presented through TauCeti.FiniteQuadraticModule.cyclic, which builds the form on ℤ/m whose generator carries a prescribed value; only the two torsion conditions on that value are checked here.

The Cartan matrices, their symmetry and their determinants are Mathlib's, in Bourbaki's numbering: the branch node of the diagram is α₄, and α₂ is the short arm.

Main declarations

• TauCeti.IntegralLattice.typeE₆RootLattice, typeE₇RootLattice, typeE₈RootLattice: the three lattices, with Gram matrices CartanMatrix.E 6, CartanMatrix.E 7, CartanMatrix.E 8.
• TauCeti.IntegralLattice.form_typeE₆SimpleRoot_typeE₆SimpleRoot and its analogues: the simple-root Gram matrix is the Cartan matrix.
• TauCeti.IntegralLattice.isEven_typeE₆RootLattice and its analogues: the lattices are even.
• TauCeti.IntegralLattice.isPosDef_typeE₆RootLattice and its analogues: they are positive definite.
• TauCeti.IntegralLattice.determinant_typeE₆RootLattice and its analogues: the determinants are 3, 2, 1.
• TauCeti.IntegralLattice.typeE₆MinusculeWeight, typeE₇MinusculeWeight: the minuscule fundamental weights ϖ₁ and ϖ₇.
• TauCeti.IntegralLattice.typeE₆DiscriminantGroupEquiv: ZMod 3 ≃+ A_{E₆}.
• TauCeti.IntegralLattice.typeE₇DiscriminantGroupEquiv: ZMod 2 ≃+ A_{E₇}.
• TauCeti.IntegralLattice.typeE₆StandardQuadraticModule and its type-E₇ analogue: the standard cyclic quadratic modules on ZMod 3 and ZMod 2.
• TauCeti.IntegralLattice.typeE₆DiscriminantQuadraticIsometry and its type-E₇ analogue: the standard cyclic modules are isometric to the corresponding discriminant forms.
• TauCeti.IntegralLattice.discriminantQuadraticMap_typeE₆MinusculeWeightClass: q(ϖ₁) = 2/3.
• TauCeti.IntegralLattice.discriminantQuadraticMap_typeE₇MinusculeWeightClass: q(ϖ₇) = 3/4.
• TauCeti.IntegralLattice.isUnimodular_typeE₈RootLattice: E₈ is unimodular, so its discriminant form is trivial.
• TauCeti.IntegralLattice.minimum_typeE₈RootLattice: E₈ has minimum 2.
• TauCeti.IntegralLattice.level_typeE₆RootLattice and its analogues: the levels are 3, 4, 1.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §8.
• W. Ebeling, Lattices and Codes, Chapters 1 and 3.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, plates V, VI, VII.

The root lattice of type E₆

noncomputable def TauCeti.IntegralLattice.typeE₆RootLattice : IntegralLattice (Fin 6 → ℚ)

The root lattice of type E₆: the rank-six integral lattice on Fin 6 → ℚ whose Gram matrix in the standard basis of simple roots is CartanMatrix.E 6.

noncomputable def TauCeti.IntegralLattice.typeE₆SimpleRoot (i : Fin 6) : Fin 6 → ℚ

The i-th simple root of the type E₆ root lattice, as a vector of the ambient space.

@[simp]

theorem TauCeti.IntegralLattice.typeE₆SimpleRoot_apply (i j : Fin 6) : typeE₆SimpleRoot i j = if j = i then 1 else 0

The i-th simple root of type E₆ is the i-th standard coordinate vector.

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₆SimpleRoot_typeE₆SimpleRoot (i j : Fin 6) : (typeE₆RootLattice.form (typeE₆SimpleRoot i)) (typeE₆SimpleRoot j) = ↑(CartanMatrix.E 6 i j)

The Gram matrix of the type E₆ root lattice in its simple-root basis is the Cartan matrix CartanMatrix.E 6.

noncomputable def TauCeti.IntegralLattice.typeE₆SimpleRootBasis : Module.Basis (Fin 6) ℤ ↥typeE₆RootLattice.carrier

The simple roots, as a ℤ-basis of the type E₆ root lattice.

@[simp]

theorem TauCeti.IntegralLattice.coe_typeE₆SimpleRootBasis_apply (i : Fin 6) : ↑(typeE₆SimpleRootBasis i) = typeE₆SimpleRoot i

The simple-root basis agrees with the ambient simple roots.

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_typeE₆SimpleRootBasis : typeE₆RootLattice.gramMatrix typeE₆SimpleRootBasis = CartanMatrix.E 6

The Gram matrix in the simple-root basis is the type E₆ Cartan matrix.

@[simp]

theorem TauCeti.IntegralLattice.integralNorm_typeE₆SimpleRootBasis (i : Fin 6) : typeE₆RootLattice.integralNorm (typeE₆SimpleRootBasis i) = 2

Each simple-root basis vector of type E₆ has squared norm 2.

@[simp]

theorem TauCeti.IntegralLattice.mem_typeE₆RootLattice_carrier_iff (x : Fin 6 → ℚ) : x ∈ typeE₆RootLattice.carrier ↔ ∀ (i : Fin 6), ∃ (z : ℤ), ↑z = x i

A vector belongs to the type E₆ root lattice exactly when all of its simple-root coordinates are integers.

instance TauCeti.IntegralLattice.instIsNondegenerateTypeE₆RootLattice : typeE₆RootLattice.IsNondegenerate

The type E₆ root lattice is nondegenerate because its Cartan matrix is nonsingular.

theorem TauCeti.IntegralLattice.isPosDef_typeE₆RootLattice : typeE₆RootLattice.IsPosDef

The type E₆ root lattice is positive definite, its Gram matrix being the positive definite Cartan matrix of the type.

theorem TauCeti.IntegralLattice.isEven_typeE₆RootLattice : typeE₆RootLattice.IsEven

The type E₆ root lattice is even: every diagonal Cartan entry is 2.

@[simp]

theorem TauCeti.IntegralLattice.determinant_typeE₆RootLattice : typeE₆RootLattice.determinant = 3

The determinant of the type E₆ root lattice is 3.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_typeE₆RootLattice : typeE₆RootLattice.discriminant = 3

The discriminant of the type E₆ root lattice is 3.

@[simp]

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_typeE₆RootLattice : Nat.card typeE₆RootLattice.DiscriminantGroup = 3

The discriminant group of the type E₆ root lattice has order 3.

The minuscule fundamental weight of type E₆

def TauCeti.IntegralLattice.typeE₆MinusculeWeight : Fin 6 → ℚ

The minuscule fundamental weight ϖ₁ of type E₆, in simple-root coordinates.

@[simp]

theorem TauCeti.IntegralLattice.typeE₆MinusculeWeight_apply (j : Fin 6) : typeE₆MinusculeWeight j = ↑(![4, 3, 5, 6, 4, 2] j) / 3

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₆MinusculeWeight_typeE₆SimpleRoot (i : Fin 6) : (typeE₆RootLattice.form typeE₆MinusculeWeight) (typeE₆SimpleRoot i) = if i = 0 then 1 else 0

The minuscule weight ϖ₁ pairs to 1 with the first simple root and to 0 with the others.

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₆MinusculeWeight_self : (typeE₆RootLattice.form typeE₆MinusculeWeight) typeE₆MinusculeWeight = 4 / 3

The self-pairing of the minuscule weight ϖ₁ of type E₆ is 4/3.

theorem TauCeti.IntegralLattice.typeE₆MinusculeWeight_mem_dualCarrier : typeE₆MinusculeWeight ∈ typeE₆RootLattice.dualCarrier

The minuscule weight ϖ₁ lies in the dual lattice: it pairs integrally with every simple root, hence with the whole lattice.

noncomputable def TauCeti.IntegralLattice.typeE₆MinusculeWeightDual : ↥typeE₆RootLattice.dualCarrier

The minuscule weight ϖ₁ of type E₆, as a vector of the dual lattice.

@[simp]

theorem TauCeti.IntegralLattice.coe_typeE₆MinusculeWeightDual : ↑typeE₆MinusculeWeightDual = typeE₆MinusculeWeight

noncomputable def TauCeti.IntegralLattice.typeE₆MinusculeWeightClass : typeE₆RootLattice.DiscriminantGroup

The discriminant class of the minuscule weight ϖ₁ of type E₆.

@[simp]

theorem TauCeti.IntegralLattice.mk_typeE₆MinusculeWeightDual : Submodule.Quotient.mk typeE₆MinusculeWeightDual = typeE₆MinusculeWeightClass

The minuscule weight ϖ₁ represents its discriminant class.

theorem TauCeti.IntegralLattice.zsmul_typeE₆MinusculeWeightClass_eq_zero_iff (k : ℤ) : k • typeE₆MinusculeWeightClass = 0 ↔ 3 ∣ k

An integer multiple of ϖ₁ lies in the type E₆ root lattice exactly when 3 divides it: the first simple-root coordinate of ϖ₁ is 4/3.

@[simp]

theorem TauCeti.IntegralLattice.addOrderOf_typeE₆MinusculeWeightClass : addOrderOf typeE₆MinusculeWeightClass = 3

The class of the minuscule weight ϖ₁ has additive order 3.

theorem TauCeti.IntegralLattice.zmultiples_typeE₆MinusculeWeightClass_eq_top : AddSubgroup.zmultiples typeE₆MinusculeWeightClass = ⊤

The class of the minuscule weight ϖ₁ generates the discriminant group of type E₆.

noncomputable def TauCeti.IntegralLattice.typeE₆DiscriminantGroupEquiv : ZMod 3 ≃+ typeE₆RootLattice.DiscriminantGroup

The discriminant group of the type E₆ root lattice is cyclic of order 3, with the class of the minuscule weight ϖ₁ as the image of 1.

@[simp]

theorem TauCeti.IntegralLattice.typeE₆DiscriminantGroupEquiv_apply_one : typeE₆DiscriminantGroupEquiv 1 = typeE₆MinusculeWeightClass

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_typeE₆MinusculeWeightClass : (typeE₆RootLattice.discriminantQuadraticMap isEven_typeE₆RootLattice) typeE₆MinusculeWeightClass = ↑(2 / 3)

The discriminant quadratic value of the minuscule weight ϖ₁ of type E₆ is 2/3, in the half-norm convention.

@[simp]

theorem TauCeti.IntegralLattice.level_typeE₆RootLattice : typeE₆RootLattice.level = 3

The level of the E₆ root lattice is 3.

@[simp]

theorem TauCeti.IntegralLattice.discriminantPairing_typeE₆MinusculeWeightClass_self : (typeE₆RootLattice.discriminantPairing typeE₆MinusculeWeightClass) typeE₆MinusculeWeightClass = ↑(1 / 3)

The discriminant bilinear value of the minuscule weight ϖ₁ of type E₆ is 1/3.

noncomputable def TauCeti.IntegralLattice.typeE₆StandardQuadraticModule : FiniteQuadraticModule

The standard cyclic quadratic module of type E₆, on ZMod 3: the generator carries the discriminant value 2/3 of the minuscule weight. The two torsion conditions demanded by the cyclic construction are 9 · (2/3) = 6 and 6 · (2/3) = 4, both integers.

@[simp]

theorem TauCeti.IntegralLattice.typeE₆StandardQuadraticModule_quadratic_one : typeE₆StandardQuadraticModule.quadratic 1 = ↑(2 / 3)

The generator of the standard type-E₆ quadratic module has value 2/3.

noncomputable def TauCeti.IntegralLattice.typeE₆DiscriminantQuadraticIsometry : typeE₆StandardQuadraticModule.Isometry (typeE₆RootLattice.discriminantQuadraticModule isEven_typeE₆RootLattice)

The standard cyclic quadratic module of type E₆ is isometric to the discriminant quadratic module of the E₆ root lattice.

@[simp]

theorem TauCeti.IntegralLattice.typeE₆DiscriminantQuadraticIsometry_toAddEquiv : typeE₆DiscriminantQuadraticIsometry.toAddEquiv = typeE₆DiscriminantGroupEquiv

The underlying additive equivalence of the type-E₆ quadratic isometry.

@[simp]

theorem TauCeti.IntegralLattice.typeE₆DiscriminantQuadraticIsometry_apply (x : ZMod 3) : typeE₆DiscriminantQuadraticIsometry x = typeE₆DiscriminantGroupEquiv x

The type-E₆ quadratic isometry acts through the discriminant-group equivalence.

The root lattice of type E₇

noncomputable def TauCeti.IntegralLattice.typeE₇RootLattice : IntegralLattice (Fin 7 → ℚ)

The root lattice of type E₇: the rank-seven integral lattice on Fin 7 → ℚ whose Gram matrix in the standard basis of simple roots is CartanMatrix.E 7.

noncomputable def TauCeti.IntegralLattice.typeE₇SimpleRoot (i : Fin 7) : Fin 7 → ℚ

The i-th simple root of the type E₇ root lattice, as a vector of the ambient space.

@[simp]

theorem TauCeti.IntegralLattice.typeE₇SimpleRoot_apply (i j : Fin 7) : typeE₇SimpleRoot i j = if j = i then 1 else 0

The i-th simple root of type E₇ is the i-th standard coordinate vector.

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₇SimpleRoot_typeE₇SimpleRoot (i j : Fin 7) : (typeE₇RootLattice.form (typeE₇SimpleRoot i)) (typeE₇SimpleRoot j) = ↑(CartanMatrix.E 7 i j)

The Gram matrix of the type E₇ root lattice in its simple-root basis is the Cartan matrix CartanMatrix.E 7.

@[simp]

theorem TauCeti.IntegralLattice.mem_typeE₇RootLattice_carrier_iff (x : Fin 7 → ℚ) : x ∈ typeE₇RootLattice.carrier ↔ ∀ (i : Fin 7), ∃ (z : ℤ), ↑z = x i

A vector belongs to the type E₇ root lattice exactly when all of its simple-root coordinates are integers.

instance TauCeti.IntegralLattice.instIsNondegenerateTypeE₇RootLattice : typeE₇RootLattice.IsNondegenerate

The type E₇ root lattice is nondegenerate because its Cartan matrix is nonsingular.

theorem TauCeti.IntegralLattice.isPosDef_typeE₇RootLattice : typeE₇RootLattice.IsPosDef

The type E₇ root lattice is positive definite, its Gram matrix being the positive definite Cartan matrix of the type.

theorem TauCeti.IntegralLattice.isEven_typeE₇RootLattice : typeE₇RootLattice.IsEven

The type E₇ root lattice is even: every diagonal Cartan entry is 2.

@[simp]

theorem TauCeti.IntegralLattice.determinant_typeE₇RootLattice : typeE₇RootLattice.determinant = 2

The determinant of the type E₇ root lattice is 2.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_typeE₇RootLattice : typeE₇RootLattice.discriminant = 2

The discriminant of the type E₇ root lattice is 2.

@[simp]

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_typeE₇RootLattice : Nat.card typeE₇RootLattice.DiscriminantGroup = 2

The discriminant group of the type E₇ root lattice has order 2.

The minuscule fundamental weight of type E₇

def TauCeti.IntegralLattice.typeE₇MinusculeWeight : Fin 7 → ℚ

The minuscule fundamental weight ϖ₇ of type E₇, in simple-root coordinates.

@[simp]

theorem TauCeti.IntegralLattice.typeE₇MinusculeWeight_apply (j : Fin 7) : typeE₇MinusculeWeight j = ↑(![2, 3, 4, 6, 5, 4, 3] j) / 2

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₇MinusculeWeight_typeE₇SimpleRoot (i : Fin 7) : (typeE₇RootLattice.form typeE₇MinusculeWeight) (typeE₇SimpleRoot i) = if i = 6 then 1 else 0

The minuscule weight ϖ₇ pairs to 1 with the seventh simple root and to 0 with the others.

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₇MinusculeWeight_self : (typeE₇RootLattice.form typeE₇MinusculeWeight) typeE₇MinusculeWeight = 3 / 2

The self-pairing of the minuscule weight ϖ₇ of type E₇ is 3/2.

theorem TauCeti.IntegralLattice.typeE₇MinusculeWeight_mem_dualCarrier : typeE₇MinusculeWeight ∈ typeE₇RootLattice.dualCarrier

The minuscule weight ϖ₇ lies in the dual lattice: it pairs integrally with every simple root, hence with the whole lattice.

noncomputable def TauCeti.IntegralLattice.typeE₇MinusculeWeightDual : ↥typeE₇RootLattice.dualCarrier

The minuscule weight ϖ₇ of type E₇, as a vector of the dual lattice.

@[simp]

theorem TauCeti.IntegralLattice.coe_typeE₇MinusculeWeightDual : ↑typeE₇MinusculeWeightDual = typeE₇MinusculeWeight

noncomputable def TauCeti.IntegralLattice.typeE₇MinusculeWeightClass : typeE₇RootLattice.DiscriminantGroup

The discriminant class of the minuscule weight ϖ₇ of type E₇.

@[simp]

theorem TauCeti.IntegralLattice.mk_typeE₇MinusculeWeightDual : Submodule.Quotient.mk typeE₇MinusculeWeightDual = typeE₇MinusculeWeightClass

The minuscule weight ϖ₇ represents its discriminant class.

theorem TauCeti.IntegralLattice.zsmul_typeE₇MinusculeWeightClass_eq_zero_iff (k : ℤ) : k • typeE₇MinusculeWeightClass = 0 ↔ 2 ∣ k

An integer multiple of ϖ₇ lies in the type E₇ root lattice exactly when 2 divides it: the second simple-root coordinate of ϖ₇ is 3/2.

@[simp]

theorem TauCeti.IntegralLattice.addOrderOf_typeE₇MinusculeWeightClass : addOrderOf typeE₇MinusculeWeightClass = 2

The class of the minuscule weight ϖ₇ has additive order 2.

theorem TauCeti.IntegralLattice.zmultiples_typeE₇MinusculeWeightClass_eq_top : AddSubgroup.zmultiples typeE₇MinusculeWeightClass = ⊤

The class of the minuscule weight ϖ₇ generates the discriminant group of type E₇.

noncomputable def TauCeti.IntegralLattice.typeE₇DiscriminantGroupEquiv : ZMod 2 ≃+ typeE₇RootLattice.DiscriminantGroup

The discriminant group of the type E₇ root lattice is cyclic of order 2, with the class of the minuscule weight ϖ₇ as the image of 1.

@[simp]

theorem TauCeti.IntegralLattice.typeE₇DiscriminantGroupEquiv_apply_one : typeE₇DiscriminantGroupEquiv 1 = typeE₇MinusculeWeightClass

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_typeE₇MinusculeWeightClass : (typeE₇RootLattice.discriminantQuadraticMap isEven_typeE₇RootLattice) typeE₇MinusculeWeightClass = ↑(3 / 4)

The discriminant quadratic value of the minuscule weight ϖ₇ of type E₇ is 3/4, in the half-norm convention.

@[simp]

theorem TauCeti.IntegralLattice.level_typeE₇RootLattice : typeE₇RootLattice.level = 4

The level of the E₇ root lattice is 4, not the exponent 2 of its discriminant group.

@[simp]

theorem TauCeti.IntegralLattice.discriminantPairing_typeE₇MinusculeWeightClass_self : (typeE₇RootLattice.discriminantPairing typeE₇MinusculeWeightClass) typeE₇MinusculeWeightClass = ↑(1 / 2)

The discriminant bilinear value of the minuscule weight ϖ₇ of type E₇ is 1/2.

noncomputable def TauCeti.IntegralLattice.typeE₇StandardQuadraticModule : FiniteQuadraticModule

The standard cyclic quadratic module of type E₇, on ZMod 2: the generator carries the discriminant value 3/4 of the minuscule weight. Here 4 is at once the square and the twice condition demanded by the cyclic construction, and 4 · (3/4) = 3 is an integer.

@[simp]

theorem TauCeti.IntegralLattice.typeE₇StandardQuadraticModule_quadratic_one : typeE₇StandardQuadraticModule.quadratic 1 = ↑(3 / 4)

The generator of the standard type-E₇ quadratic module has value 3/4.

noncomputable def TauCeti.IntegralLattice.typeE₇DiscriminantQuadraticIsometry : typeE₇StandardQuadraticModule.Isometry (typeE₇RootLattice.discriminantQuadraticModule isEven_typeE₇RootLattice)

The standard cyclic quadratic module of type E₇ is isometric to the discriminant quadratic module of the E₇ root lattice.

@[simp]

theorem TauCeti.IntegralLattice.typeE₇DiscriminantQuadraticIsometry_toAddEquiv : typeE₇DiscriminantQuadraticIsometry.toAddEquiv = typeE₇DiscriminantGroupEquiv

The underlying additive equivalence of the type-E₇ quadratic isometry.

@[simp]

theorem TauCeti.IntegralLattice.typeE₇DiscriminantQuadraticIsometry_apply (x : ZMod 2) : typeE₇DiscriminantQuadraticIsometry x = typeE₇DiscriminantGroupEquiv x

The type-E₇ quadratic isometry acts through the discriminant-group equivalence.

The root lattice of type E₈

noncomputable def TauCeti.IntegralLattice.typeE₈RootLattice : IntegralLattice (Fin 8 → ℚ)

The root lattice of type E₈: the rank-eight integral lattice on Fin 8 → ℚ whose Gram matrix in the standard basis of simple roots is CartanMatrix.E 8.

theorem TauCeti.IntegralLattice.typeE₈RootLattice_def : typeE₈RootLattice = ofGramMatrix (Pi.basisFun ℚ (Fin 8)) (CartanMatrix.E 8) ⋯

The type E₈ root lattice is the Gram-matrix lattice of CartanMatrix.E 8 in standard coordinates.

theorem TauCeti.IntegralLattice.norm_typeE₈RootLattice_intCast (v : Fin 8 → ℤ) : (typeE₈RootLattice.norm fun (j : Fin 8) => ↑(v j)) = ↑(Matrix.vecMul v (CartanMatrix.E 8) ⬝ᵥ v)

The rational norm of an integer vector in simple-root coordinates is its integral Cartan norm.

theorem TauCeti.IntegralLattice.form_typeE₈RootLattice_intCast (u w : Fin 8 → ℤ) : ((typeE₈RootLattice.form fun (j : Fin 8) => ↑(u j)) fun (j : Fin 8) => ↑(w j)) = ↑(Matrix.vecMul u (CartanMatrix.E 8) ⬝ᵥ w)

The rational form of two integer vectors in simple-root coordinates is their integral Cartan form.

noncomputable def TauCeti.IntegralLattice.typeE₈SimpleRoot (i : Fin 8) : Fin 8 → ℚ

The i-th simple root of the type E₈ root lattice, as a vector of the ambient space.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈SimpleRoot_apply (i j : Fin 8) : typeE₈SimpleRoot i j = if j = i then 1 else 0

The i-th simple root of type E₈ is the i-th standard coordinate vector.

theorem TauCeti.IntegralLattice.typeE₈SimpleRoot_eq_basisFun (i : Fin 8) : typeE₈SimpleRoot i = (Pi.basisFun ℚ (Fin 8)) i

The i-th simple root of type E₈ is the i-th standard basis vector.

@[simp]

theorem TauCeti.IntegralLattice.form_typeE₈SimpleRoot_typeE₈SimpleRoot (i j : Fin 8) : (typeE₈RootLattice.form (typeE₈SimpleRoot i)) (typeE₈SimpleRoot j) = ↑(CartanMatrix.E 8 i j)

The Gram matrix of the type E₈ root lattice in its simple-root basis is the Cartan matrix CartanMatrix.E 8.

theorem TauCeti.IntegralLattice.typeE₈RootLattice_carrier : typeE₈RootLattice.carrier = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℚ (Fin 8)))

The carrier of the type E₈ root lattice is the integral span of the simple roots.

@[simp]

theorem TauCeti.IntegralLattice.mem_typeE₈RootLattice_carrier_iff (x : Fin 8 → ℚ) : x ∈ typeE₈RootLattice.carrier ↔ ∀ (i : Fin 8), ∃ (z : ℤ), ↑z = x i

A vector belongs to the type E₈ root lattice exactly when all of its simple-root coordinates are integers.

instance TauCeti.IntegralLattice.instIsNondegenerateTypeE₈RootLattice : typeE₈RootLattice.IsNondegenerate

The type E₈ root lattice is nondegenerate because its Cartan matrix is nonsingular.

theorem TauCeti.IntegralLattice.isPosDef_typeE₈RootLattice : typeE₈RootLattice.IsPosDef

The type E₈ root lattice is positive definite, its Gram matrix being the positive definite Cartan matrix of the type.

theorem TauCeti.IntegralLattice.isEven_typeE₈RootLattice : typeE₈RootLattice.IsEven

The type E₈ root lattice is even: every diagonal Cartan entry is 2.

theorem TauCeti.IntegralLattice.minimum_typeE₈RootLattice : typeE₈RootLattice.minimum = 2

The type E₈ root lattice has minimum 2: it is even and positive definite, and its simple roots are roots, of norm 2.

@[simp]

theorem TauCeti.IntegralLattice.determinant_typeE₈RootLattice : typeE₈RootLattice.determinant = 1

The determinant of the type E₈ root lattice is 1.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_typeE₈RootLattice : typeE₈RootLattice.discriminant = 1

The discriminant of the type E₈ root lattice is 1.

theorem TauCeti.IntegralLattice.isUnimodular_typeE₈RootLattice : typeE₈RootLattice.IsUnimodular

The type E₈ root lattice is unimodular: its Cartan determinant is 1.

@[simp]

theorem TauCeti.IntegralLattice.level_typeE₈RootLattice : typeE₈RootLattice.level = 1

The even unimodular E₈ root lattice has level 1.

@[simp]

theorem TauCeti.IntegralLattice.dualCarrier_typeE₈RootLattice : typeE₈RootLattice.dualCarrier = typeE₈RootLattice.carrier

The type E₈ root lattice is self-dual.

instance TauCeti.IntegralLattice.instSubsingletonDiscriminantGroupTypeE₈RootLattice : Subsingleton typeE₈RootLattice.DiscriminantGroup

The discriminant group of the type E₈ root lattice is trivial.

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_typeE₈RootLattice : Nat.card typeE₈RootLattice.DiscriminantGroup = 1

The discriminant group of the type E₈ root lattice has order 1.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_typeE₈RootLattice (x : typeE₈RootLattice.DiscriminantGroup) : (typeE₈RootLattice.discriminantQuadraticMap isEven_typeE₈RootLattice) x = 0

The discriminant quadratic form of the type E₈ root lattice is trivial, its discriminant group having a single element.