The Coxeter matrix of a Dynkin type

TauCeti.coxeterMatrixOfBase reads a Coxeter matrix off the Cartan matrix of a base, entry by entry: the order of the product of two simple reflections is the Cartan product of the two simple roots, translated by 0 ↦ 2, 1 ↦ 3, 2 ↦ 4, 3 ↦ 6. This file performs that translation on the standard Cartan matrices of TauCeti.DynkinType, so that a base matched to a Dynkin type carries a named Coxeter matrix, and identifies the outcome with the finite-type Coxeter matrices CoxeterMatrix.A, .B, .E₆, .E₇, .E₈, .F₄ and .G₂ that Mathlib already pins.

The identifications are worth spelling out one type at a time because they supply the matrix-level part of the classification's acceptance criteria: in the Bourbaki numbering, type Aₙ gives CoxeterMatrix.A n. The Bₙ/Cₙ pair collapses here: transposing a Cartan matrix leaves every Cartan product fixed, so the two types, which are distinct root systems with transposed Cartan matrices, share the single Coxeter matrix CoxeterMatrix.B n. That collapse is exactly the information the Coxeter matrix drops — it records the diagram and its edge multiplicities, but not the direction of a multiple edge.

Type Dₙ is the one type this file matches to no Mathlib matrix, CoxeterMatrix.D n not being the Coxeter matrix of type Dₙ: alongside the fork edge between the nodes n - 3 and n - 1 it keeps the chain edge between the two fork nodes n - 2 and n - 1, so its diagram carries n edges on n nodes and contains a triangle, while a Dynkin diagram is a tree. TauCeti.DynkinType.coxeterMatrix_D_apply describes the type Dₙ entries directly instead, and TauCeti.DynkinType.coxeterMatrix_D_ne_coxeterMatrix_D records that the two matrices differ, in the Bourbaki numbering, at that pair of fork nodes.

Main definitions

• TauCeti.DynkinType.coxeterMatrix: the standard Coxeter matrix of a Dynkin type, in the same Bourbaki node numbering as TauCeti.DynkinType.cartanMatrix.

Main results

• TauCeti.DynkinType.cartanMatrix_mul_cartanMatrix_mem_of_ne: the Cartan product of two distinct nodes of a standard Cartan matrix lies in {0, 1, 2, 3}, each standard matrix being of finite type. This is what makes the Coxeter matrix above well defined.
• TauCeti.DynkinType.coxeterMatrix_apply_of_isSimplyLaced: on a simply-laced type the Coxeter entry is 2 at an orthogonal pair of nodes and 3 at an adjacent one, so the Coxeter matrix is the diagram itself.
• TauCeti.DynkinType.coxeterMatrix_A, _B, _C, _E6, _E7, _E8, _F4, _G2: the standard Coxeter matrix of each type, identified with Mathlib's, together with TauCeti.DynkinType.coxeterMatrix_D_apply for type Dₙ.
• TauCeti.coxeterMatrixOfBase_eq_coxeterMatrix_reindex: the Coxeter matrix of a base is the standard Coxeter matrix of a type, under any relabelling of the simple roots by the Bourbaki nodes that matches the two Cartan matrices, and TauCeti.HasCartanType.exists_coxeterMatrixOfBase_eq, its existential form for a base of Cartan type t. Its corollaries TauCeti.HasCartanType.exists_coxeterMatrixOfBase_eq_A and TauCeti.HasCartanType.exists_coxeterMatrixOfBase_eq_G2 are the two the roadmap names.

References

This file supplies the clause "recovering CoxeterMatrix.A n as coxeterMatrixOfBase b" of the Aₙ worked example, and its G₂ counterpart, in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, bridging the coxeterMatrixOfBase of Layer 2 and the DynkinType enumeration of Layer 5. The translation of a Cartan product into a Coxeter order is Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI, §1.3, and Humphreys, Introduction to Lie Algebras and Representation Theory, §9.4 and §11.4.

The Cartan products of a standard Cartan matrix

theorem TauCeti.DynkinType.cartanMatrix_mul_cartanMatrix_mem_of_ne (t : DynkinType) {i j : Fin t.rank} (hij : i ≠ j) : t.cartanMatrix i j * t.cartanMatrix j i ∈ {0, 1, 2, 3}

The Cartan product of two distinct nodes of a Dynkin type lies in {0, 1, 2, 3}, the four values that name the orders 2, 3, 4, 6 of a product of two simple reflections. Validity of the type is not needed: the degenerate members of the families are of finite type as well, and the bound is the finite-type bound TauCeti.IsFiniteType.apply_mul_apply_mem_of_ne.

The Coxeter matrix of a type

def TauCeti.DynkinType.coxeterMatrix (t : DynkinType) : CoxeterMatrix (Fin t.rank)

The standard Coxeter matrix of a Dynkin type, indexed by Fin t.rank in the Bourbaki node numbering of TauCeti.DynkinType.cartanMatrix: it is TauCeti.coxeterMatrixOfCartanMatrix applied to the standard Cartan matrix, so the entry at a pair of nodes is TauCeti.coxeterOrder of their Cartan product.

The body is not exposed: TauCeti.DynkinType.coxeterMatrix_apply is the entry API.

Equations

• t.coxeterMatrix = TauCeti.coxeterMatrixOfCartanMatrix t.cartanMatrix ⋯ ⋯

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_apply (t : DynkinType) (i j : Fin t.rank) : t.coxeterMatrix.M i j = coxeterOrder (t.cartanMatrix i j * t.cartanMatrix j i)

The entry of the standard Coxeter matrix of a type at a pair of nodes is TauCeti.coxeterOrder applied to the product of the two Cartan entries.

theorem TauCeti.DynkinType.coxeterMatrix_apply_eq_two_iff (t : DynkinType) {i j : Fin t.rank} (hij : i ≠ j) : t.coxeterMatrix.M i j = 2 ↔ t.cartanMatrix i j = 0

Two nodes carry the Coxeter entry 2 exactly when they are not joined: the two simple reflections commute exactly when the two simple roots are orthogonal.

theorem TauCeti.DynkinType.coxeterMatrix_apply_of_isSimplyLaced {t : DynkinType} (ht : t.cartanMatrix.IsSimplyLaced) {i j : Fin t.rank} (hij : i ≠ j) : t.coxeterMatrix.M i j = if t.cartanMatrix i j = 0 then 2 else 3

On a simply-laced type the Coxeter matrix is the diagram: distinct nodes carry the entry 2 when they are not joined and 3 when they are, there being no multiple edge to raise an entry to 4 or 6.

The Coxeter matrix of each type

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_A (n : ℕ) : (A n).coxeterMatrix = CoxeterMatrix.A n

Type Aₙ has Coxeter matrix CoxeterMatrix.A n, the chain of n nodes with every edge labelled 3.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_B (n : ℕ) : (B n).coxeterMatrix = CoxeterMatrix.B n

Type Bₙ has Coxeter matrix CoxeterMatrix.B n, the chain of n nodes whose last edge is labelled 4.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_C (n : ℕ) : (C n).coxeterMatrix = CoxeterMatrix.B n

Type Cₙ has the same Coxeter matrix as type Bₙ. The two standard Cartan matrices are transposes of one another, and a Cartan product is invariant under transposition, so the Coxeter matrix cannot separate them: it records the double edge but not its direction. The two types are nonetheless distinct root systems, dual to one another.

theorem TauCeti.DynkinType.coxeterMatrix_D_apply (n : ℕ) {i j : Fin (D n).rank} (hij : i ≠ j) : (D n).coxeterMatrix.M i j = if CartanMatrix.D n i j = 0 then 2 else 3

The Coxeter entries of type Dₙ: 3 between two nodes joined in the diagram and 2 between two nodes that are not, type Dₙ being simply laced.

Mathlib's CoxeterMatrix.D n is not this matrix; see TauCeti.DynkinType.coxeterMatrix_D_ne_coxeterMatrix_D.

theorem TauCeti.DynkinType.coxeterMatrix_D_ne_coxeterMatrix_D {n : ℕ} (hn : 4 ≤ n) : (D n).coxeterMatrix ≠ CoxeterMatrix.D n

Mathlib's CoxeterMatrix.D n is not the Coxeter matrix of type Dₙ in the Bourbaki numbering. The two differ at the pair n - 2, n - 1 of fork nodes: the Cartan entry of type Dₙ vanishes there, both nodes being joined to the branch node n - 3 instead, while CoxeterMatrix.D n labels that pair with a 3, it being consecutive — on top of the fork edge it adds between n - 3 and n - 1. Its diagram therefore carries n edges on n nodes and is no tree, so no relabelling matches it to the diagram of Dₙ either; it is the inequality in the Bourbaki numbering that is recorded here.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_E6 : E6.coxeterMatrix = CoxeterMatrix.E₆

Type E₆ has Coxeter matrix CoxeterMatrix.E₆.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_E7 : E7.coxeterMatrix = CoxeterMatrix.E₇

Type E₇ has Coxeter matrix CoxeterMatrix.E₇.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_E8 : E8.coxeterMatrix = CoxeterMatrix.E₈

Type E₈ has Coxeter matrix CoxeterMatrix.E₈.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_F4 : F4.coxeterMatrix = CoxeterMatrix.F₄

Type F₄ has Coxeter matrix CoxeterMatrix.F₄, the chain of four nodes with the middle edge labelled 4.

@[simp]

theorem TauCeti.DynkinType.coxeterMatrix_G2 : G2.coxeterMatrix = CoxeterMatrix.G₂

Type G₂ has Coxeter matrix CoxeterMatrix.G₂, the single edge labelled 6. The standard Cartan matrix of G₂ is the transpose of Mathlib's, a difference the Cartan product does not see.

The Coxeter matrix of a base of a given Cartan type

theorem TauCeti.coxeterMatrixOfBase_eq_coxeterMatrix_reindex {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] {b : P.Base} {t : DynkinType} (e : ↥b.support ≃ Fin t.rank) (he : ∀ (i j : ↥b.support), b.cartanMatrix i j = t.cartanMatrix (e i) (e j)) : coxeterMatrixOfBase P b = CoxeterMatrix.reindex e.symm t.coxeterMatrix

The Coxeter matrix of a base is the standard Coxeter matrix of a type, under any relabelling of the simple roots by the Bourbaki nodes that matches the two Cartan matrices. Reading a Coxeter matrix off a Cartan matrix is entrywise, so a relabelling matching the Cartan entries matches the Coxeter entries too — the same relabelling, so that a caller holding a Cartan-matching e keeps it rather than being handed a new one.

Combined with the identifications above, this shows that a base of type Aₙ carries CoxeterMatrix.A n, one of type Bₙ or Cₙ carries CoxeterMatrix.B n, and so on.

theorem TauCeti.HasCartanType.exists_coxeterMatrixOfBase_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] {b : P.Base} {t : DynkinType} (h : HasCartanType P b t) : ∃ (e : ↥b.support ≃ Fin t.rank), coxeterMatrixOfBase P b = CoxeterMatrix.reindex e.symm t.coxeterMatrix

The Coxeter matrix of a base of Cartan type t is the standard Coxeter matrix of t, after a relabelling of the simple roots by the Bourbaki nodes. Any relabelling matching the two Cartan matrices will do, by TauCeti.coxeterMatrixOfBase_eq_coxeterMatrix_reindex; this existential is the form the type-by-type corollaries below take.

theorem TauCeti.HasCartanType.exists_coxeterMatrixOfBase_eq_A {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] {b : P.Base} {n : ℕ} (h : HasCartanType P b (DynkinType.A n)) : ∃ (e : ↥b.support ≃ Fin n), coxeterMatrixOfBase P b = CoxeterMatrix.reindex e.symm (CoxeterMatrix.A n)

A base of type Aₙ carries the Coxeter matrix CoxeterMatrix.A n, after relabelling its simple roots by the Bourbaki nodes.

theorem TauCeti.HasCartanType.exists_coxeterMatrixOfBase_eq_G2 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] {b : P.Base} (h : HasCartanType P b DynkinType.G2) : ∃ (e : ↥b.support ≃ Fin 2), coxeterMatrixOfBase P b = CoxeterMatrix.reindex e.symm CoxeterMatrix.G₂

A base of type G₂ carries the Coxeter matrix CoxeterMatrix.G₂, the single edge labelled 6.