The root lattice of a simply-laced Dynkin type

For a simply-laced Dynkin type t (types A, D, E₆, E₇, E₈), the Cartan matrix t.cartanMatrix is symmetric and positive definite, so it is the Gram matrix of a positive definite integral lattice. This file constructs that lattice uniformly in t,

t.rootLattice ht = ℤ^{rank t} ⊆ ℚ^{rank t},   ⟨x, y⟩ = xᵀ (cartanMatrix t) y,

so that the standard coordinate vectors are the simple roots in Bourbaki numbering. It proves the properties every orthogonal sum of such lattices inherits: the simple roots form a ℤ-basis with Gram matrix t.cartanMatrix, the lattice has rank t.rank, it is even and positive definite, its determinant is det t.cartanMatrix, and its norm-2 vectors span the whole carrier.

Uniformity is the point of the construction: an ordered list of ADE components is a list of Dynkin types, and the orthogonal sum of their root lattices has to be formed without a case split on each component. The case split is done once, here, by identifying the uniform lattice with the family-specific models that carry the discriminant-form computations:

• (A n).rootLattice _ and the three exceptional lattices are literally the simple-root lattices TauCeti.IntegralLattice.typeARootLattice n, typeE₆RootLattice, typeE₇RootLattice and typeE₈RootLattice;
• for 4 ≤ n, (D n).rootLattice _ is isometric to the Conway--Sloane checkerboard lattice TauCeti.IntegralLattice.checkerboardLattice n, by the isometry sending the i-th simple root to the i-th Bourbaki simple root TauCeti.IntegralLattice.checkerboardSimpleRoot n hn i.

The hypothesis is that the type is simply laced. Only the symmetry and positive definiteness of the Cartan matrix are used, and these also hold for the degenerate names B 0, B 1, C 0 and C 1, whose matrices are those of type A; those names are not types of root systems, so they are excluded here (TauCeti.DynkinType.isSimplyLaced_cartanMatrix_iff).

Main declarations

• TauCeti.DynkinType.rootLattice: the positive root lattice of a simply-laced Dynkin type.
• TauCeti.DynkinType.simpleRootBasis: its simple-root ℤ-basis.
• TauCeti.DynkinType.gramMatrix_simpleRootBasis: the Gram matrix of that basis is the Cartan matrix.
• TauCeti.DynkinType.finrank_rootLattice, isEven_rootLattice, isPosDef_rootLattice, determinant_rootLattice, minimum_rootLattice: rank, evenness, positive definiteness, determinant and minimum.
• TauCeti.DynkinType.span_vectorsOfNorm_two_rootLattice: the norm-2 vectors span the carrier.
• TauCeti.DynkinType.eq_rootLattice: a lattice with integral coordinates and Cartan Gram matrix is the root lattice.
• TauCeti.DynkinType.rootLatticeIsometryOfEq: the isometry between the root lattices of equal Dynkin types.
• TauCeti.DynkinType.rootLattice_A, rootLattice_E6, rootLattice_E7, rootLattice_E8: identification with the family-specific simple-root lattices.
• TauCeti.DynkinType.rootLatticeIsometryCheckerboard: the isometry of the type Dₙ root lattice with the checkerboard lattice.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates I--VII, for the Cartan matrices and the simple-root numbering.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §§6--8, for the root lattices Aₙ, Dₙ, E₆, E₇, E₈.

noncomputable def TauCeti.DynkinType.rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : IntegralLattice (Fin t.rank → ℚ)

The positive root lattice of a simply-laced Dynkin type t: the integral lattice on Fin t.rank → ℚ whose Gram matrix in the standard basis is the Cartan matrix t.cartanMatrix. The standard coordinate vectors are the simple roots, in Bourbaki numbering.

theorem TauCeti.DynkinType.rootLattice_carrier (t : DynkinType) (ht : t.IsSimplyLaced) : (t.rootLattice ht).carrier = Submodule.span ℤ (Set.range fun (i : Fin t.rank) => Pi.single i 1)

The carrier of the root lattice is the ℤ-span of the standard coordinate vectors, the simple roots.

@[simp]

theorem TauCeti.DynkinType.mem_rootLattice_carrier_iff (t : DynkinType) (ht : t.IsSimplyLaced) (x : Fin t.rank → ℚ) : x ∈ (t.rootLattice ht).carrier ↔ ∀ (i : Fin t.rank), ∃ (z : ℤ), ↑z = x i

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

theorem TauCeti.DynkinType.rootLattice_form_apply (t : DynkinType) (ht : t.IsSimplyLaced) (x y : Fin t.rank → ℚ) : ((t.rootLattice ht).form x) y = ∑ i : Fin t.rank, x i * ∑ j : Fin t.rank, ↑(t.cartanMatrix i j) * y j

The form of the root lattice, expanded in simple-root coordinates.

theorem TauCeti.DynkinType.norm_rootLattice_intCast (t : DynkinType) (ht : t.IsSimplyLaced) (v : Fin t.rank → ℤ) : ((t.rootLattice ht).norm fun (j : Fin t.rank) => ↑(v j)) = ↑(Matrix.vecMul v t.cartanMatrix ⬝ᵥ v)

The rational norm of an integer vector of the root lattice is its integral Cartan norm vᵀ (cartanMatrix t) v.

theorem TauCeti.DynkinType.form_rootLattice_intCast (t : DynkinType) (ht : t.IsSimplyLaced) (u w : Fin t.rank → ℤ) : (((t.rootLattice ht).form fun (j : Fin t.rank) => ↑(u j)) fun (j : Fin t.rank) => ↑(w j)) = ↑(Matrix.vecMul u t.cartanMatrix ⬝ᵥ w)

The rational form of two integer vectors of the root lattice is their integral Cartan form uᵀ (cartanMatrix t) w.

noncomputable def TauCeti.DynkinType.simpleRootBasis (t : DynkinType) (ht : t.IsSimplyLaced) : Module.Basis (Fin t.rank) ℤ ↥(t.rootLattice ht).carrier

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

@[simp]

theorem TauCeti.DynkinType.coe_simpleRootBasis (t : DynkinType) (ht : t.IsSimplyLaced) (i : Fin t.rank) : ↑((t.simpleRootBasis ht) i) = Pi.single i 1

The i-th simple root is the i-th standard coordinate vector.

@[simp]

theorem TauCeti.DynkinType.gramMatrix_simpleRootBasis (t : DynkinType) (ht : t.IsSimplyLaced) : (t.rootLattice ht).gramMatrix (t.simpleRootBasis ht) = t.cartanMatrix

The Gram matrix of the root lattice in its simple-root basis is the Cartan matrix.

@[simp]

theorem TauCeti.DynkinType.rootLattice_form_single_single (t : DynkinType) (ht : t.IsSimplyLaced) (i j : Fin t.rank) : ((t.rootLattice ht).form (Pi.single i 1)) (Pi.single j 1) = ↑(t.cartanMatrix i j)

The pairing of two simple roots is the corresponding Cartan integer.

@[simp]

theorem TauCeti.DynkinType.finrank_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : Module.finrank ℤ ↥(t.rootLattice ht).carrier = t.rank

The root lattice of t has rank t.rank.

theorem TauCeti.DynkinType.isEven_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : (t.rootLattice ht).IsEven

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

theorem TauCeti.DynkinType.isPosDef_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : (t.rootLattice ht).IsPosDef

The root lattice is positive definite, the Cartan matrix of a simply-laced type being positive definite.

instance TauCeti.DynkinType.instIsNondegenerateForallFinRankRatRootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : (t.rootLattice ht).IsNondegenerate

The root lattice is nondegenerate, being positive definite.

@[simp]

theorem TauCeti.DynkinType.determinant_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : (t.rootLattice ht).determinant = t.cartanMatrix.det

The determinant of the root lattice is the determinant of the Cartan matrix.

@[simp]

theorem TauCeti.DynkinType.rootLattice_norm_single (t : DynkinType) (ht : t.IsSimplyLaced) (i : Fin t.rank) : (t.rootLattice ht).norm (Pi.single i 1) = 2

Every simple root has norm 2.

theorem TauCeti.DynkinType.span_vectorsOfNorm_two_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) : Submodule.span ℤ ((fun (x : ↥(t.rootLattice ht).carrier) => ↑x) '' (t.rootLattice ht).vectorsOfNorm 2) = (t.rootLattice ht).carrier

The norm-2 vectors of the root lattice span its carrier: the simple roots have norm 2 and form a ℤ-basis.

@[simp]

theorem TauCeti.DynkinType.minimum_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) (h : t.rank ≠ 0) : (t.rootLattice ht).minimum = 2

A root lattice of positive rank has minimum 2: it is even and a simple root has norm 2.

noncomputable def TauCeti.DynkinType.rootLatticeIsometryOfEq (t : DynkinType) (ht : t.IsSimplyLaced) {s : DynkinType} (h : t = s) (hs : s.IsSimplyLaced) : (t.rootLattice ht).Isometry (s.rootLattice hs)

Root lattices of equal Dynkin types are isometric: for h : t = s, the isometry from the root lattice of t to that of s which reads simple-root coordinates along the equality of ranks. It lets a family of components that is only propositionally equal to another one, such as the components of a list read off by position, be compared with it.

@[simp]

theorem TauCeti.DynkinType.rootLatticeIsometryOfEq_rfl (t : DynkinType) (ht : t.IsSimplyLaced) : t.rootLatticeIsometryOfEq ht ⋯ ht = IntegralLattice.Isometry.refl (t.rootLattice ht)

The isometry of the root lattice of t with itself is the identity.

@[simp]

theorem TauCeti.DynkinType.rootLatticeIsometryOfEq_apply (t : DynkinType) (ht : t.IsSimplyLaced) {s : DynkinType} (h : t = s) (hs : s.IsSimplyLaced) (x : Fin t.rank → ℚ) (j : Fin s.rank) : (t.rootLatticeIsometryOfEq ht h hs) x j = x (Fin.cast ⋯ j)

The isometry of root lattices of equal types reads each simple-root coordinate of the target from the corresponding coordinate of the source.

Identification with the family-specific models

theorem TauCeti.DynkinType.eq_rootLattice (t : DynkinType) (ht : t.IsSimplyLaced) {L : IntegralLattice (Fin t.rank → ℚ)} (hcarrier : ∀ (x : Fin t.rank → ℚ), x ∈ L.carrier ↔ ∀ (i : Fin t.rank), ∃ (z : ℤ), ↑z = x i) (hform : ∀ (i j : Fin t.rank), (L.form (Pi.single i 1)) (Pi.single j 1) = ↑(t.cartanMatrix i j)) : L = t.rootLattice ht

Characterization of the root lattice: an integral lattice on Fin t.rank → ℚ whose carrier is the standard integral lattice ℤ^{rank t}, and whose form pairs the standard basis vectors by the Cartan integers, is the root lattice of t.

theorem TauCeti.DynkinType.rootLattice_A (n : ℕ) (ht : (A n).IsSimplyLaced) : (A n).rootLattice ht = IntegralLattice.typeARootLattice n

The root lattice of type Aₙ is the simple-root lattice typeARootLattice n.

theorem TauCeti.DynkinType.rootLattice_E6 (ht : E6.IsSimplyLaced) : E6.rootLattice ht = IntegralLattice.typeE₆RootLattice

The root lattice of type E₆ is the simple-root lattice typeE₆RootLattice.

theorem TauCeti.DynkinType.rootLattice_E7 (ht : E7.IsSimplyLaced) : E7.rootLattice ht = IntegralLattice.typeE₇RootLattice

The root lattice of type E₇ is the simple-root lattice typeE₇RootLattice.

theorem TauCeti.DynkinType.rootLattice_E8 (ht : E8.IsSimplyLaced) : E8.rootLattice ht = IntegralLattice.typeE₈RootLattice

The root lattice of type E₈ is the simple-root lattice typeE₈RootLattice.

noncomputable def TauCeti.DynkinType.rootLatticeIsometryCheckerboard (n : ℕ) (hn : 4 ≤ n) (ht : (D n).IsSimplyLaced) : ((D n).rootLattice ht).Isometry (IntegralLattice.checkerboardLattice n)

The root lattice of type Dₙ is the checkerboard lattice. For 4 ≤ n, the isometry sends the i-th simple root to the i-th Bourbaki simple root of the Conway--Sloane coordinate model {x ∈ ℤⁿ | ∑ xᵢ even}; both bases have Gram matrix CartanMatrix.D n.

theorem TauCeti.DynkinType.rootLatticeIsometryCheckerboard_single (n : ℕ) (hn : 4 ≤ n) (ht : (D n).IsSimplyLaced) (i : Fin n) : (rootLatticeIsometryCheckerboard n hn ht) (Pi.single i 1) = IntegralLattice.checkerboardSimpleRoot n hn i

The isometry rootLatticeIsometryCheckerboard sends the i-th simple root to the i-th Bourbaki simple root of the checkerboard lattice.