The Coxeter matrix of a base

A base of a finite crystallographic root pairing has a Cartan matrix, and the Cartan matrix determines a Coxeter matrix: the entry attached to a pair of distinct simple roots is read off their Cartan product ⟨αᵢ, αⱼ^∨⟩⟨αⱼ, αᵢ^∨⟩ by 0 ↦ 2, 1 ↦ 3, 2 ↦ 4, 3 ↦ 6. This file proves that the Cartan product of two distinct simple roots really does lie in {0, 1, 2, 3}, and packages the resulting assignment as a genuine CoxeterMatrix indexed by the simple roots.

The numerical content is the exclusion of the value 4. Mathlib bounds the Coxeter weight of a finite crystallographic pairing by 4 and pins it to {0, 1, 2, 3, 4} (RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic), and the value 4 is attained exactly by linearly dependent pairs of roots (RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four); distinct simple roots are independent, so 4 is unavailable to them.

The translation TauCeti.coxeterOrder is defined on all of ℤ and takes the Cartan product 4 to 1, which is the mathematically correct value rather than a junk one: product 4 means the two roots are proportional, so the two reflections coincide and their product is the identity. That choice is what makes the diagonal of the matrix come out as 1 without a case split, since a simple root has Cartan product 4 with itself. Products outside {0, 1, 2, 3, 4} do not occur here and are sent to 0, Mathlib's encoding of an infinite Coxeter order.

The final section checks the smallest of the intended braid relations, the one available before the Coxeter presentation of the Weyl group is built: an entry is 2 exactly for orthogonal simple roots, and there the two simple reflections commute (RootPairing.weylGroup.commute_ofIdx_of_isOrthogonal) and their product has order exactly 2, as the entry asserts.

Main definitions

• TauCeti.coxeterOrder translates a Cartan product into the order of the product of the two reflections.
• TauCeti.coxeterMatrixOfCartanMatrix performs that translation on an arbitrary matrix whose diagonal is 2 and whose off-diagonal Cartan products lie in {0, 1, 2, 3}.
• TauCeti.coxeterMatrixOfBase is the Coxeter matrix of a base, indexed by its simple roots.

Main results

• TauCeti.cartanMatrix_mul_cartanMatrix_mem_of_ne: the Cartan product of two distinct simple roots lies in {0, 1, 2, 3}, so TauCeti.coxeterOrder reads a genuine Coxeter order off it.
• TauCeti.coxeterMatrixOfBase_eq_two_iff: an entry is 2 exactly for orthogonal simple roots. In particular the diagonal entries are not 2, since no root is orthogonal to itself.
• TauCeti.isSimplyLaced_iff_forall_coxeterMatrixOfBase_le_three: the Cartan matrix is simply laced exactly when all entries are at most 3.
• TauCeti.coxeterMatrixOfBase_eq_three_of_hasCartanType_A_two and its B₂ and G₂ companions evaluate the Coxeter entries of the three rank-two Cartan types.
• RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_two_of_coxeterMatrixOfBase_eq_two: where the matrix entry is 2, the product of the two simple reflections does have order 2.

References

This file implements “The Coxeter matrix of a base” in Layer 2 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signature coxeterMatrixOfBase in that roadmap's Suggested.lean. The classification of rank-two crystallographic configurations behind it is Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.3.

Reading a Coxeter order off a Cartan product

def TauCeti.coxeterOrder (c : ℤ) : ℕ

The order of the product of the reflections in two roots of Cartan product c.

For a finite crystallographic pairing the only products that occur are 0, 1, 2, 3 and 4. The first four are the rank-two configurations A₁ × A₁, A₂, B₂ and G₂, whose products of reflections are rotations of order 2, 3, 4 and 6. Product 4 means the two roots are proportional, so the two reflections agree and their product is the identity, of order 1; this is in particular the value taken by a root against itself. Every other integer is sent to 0, Mathlib's encoding of an infinite order.

Equations

• TauCeti.coxeterOrder c = if c = 0 then 2 else if c = 1 then 3 else if c = 2 then 4 else if c = 3 then 6 else if c = 4 then 1 else 0

@[simp]

theorem TauCeti.coxeterOrder_zero : coxeterOrder 0 = 2

@[simp]

theorem TauCeti.coxeterOrder_one : coxeterOrder 1 = 3

@[simp]

theorem TauCeti.coxeterOrder_two : coxeterOrder 2 = 4

@[simp]

theorem TauCeti.coxeterOrder_three : coxeterOrder 3 = 6

@[simp]

theorem TauCeti.coxeterOrder_four : coxeterOrder 4 = 1

theorem TauCeti.coxeterOrder_eq_zero_iff {c : ℤ} : coxeterOrder c = 0 ↔ c ∉ {0, 1, 2, 3, 4}

Outside {0, 1, 2, 3, 4} the translation falls back to 0, Mathlib's encoding of an infinite order. No such Cartan product occurs for a finite crystallographic pairing; this lemma pins the value down at the remaining integers, so the five equation lemmas above determine coxeterOrder everywhere.

theorem TauCeti.coxeterOrder_mem {c : ℤ} (hc : c ∈ {0, 1, 2, 3}) : coxeterOrder c ∈ {2, 3, 4, 6}

On the products that occur for a pair of independent roots, coxeterOrder takes the four dihedral values.

theorem TauCeti.two_le_coxeterOrder {c : ℤ} (hc : c ∈ {0, 1, 2, 3}) : 2 ≤ coxeterOrder c

The dihedral values are all at least 2; in particular none of them is 1, which is what a CoxeterMatrix demands off the diagonal.

theorem TauCeti.coxeterOrder_le_six {c : ℤ} (hc : c ∈ {0, 1, 2, 3}) : coxeterOrder c ≤ 6

The dihedral values are all at most 6; in particular none of them is 0, so no entry of the Coxeter matrix of a base is infinite.

theorem TauCeti.coxeterOrder_le_three_iff {c : ℤ} (hc : c ∈ {0, 1, 2, 3}) : coxeterOrder c ≤ 3 ↔ c = 0 ∨ c = 1

The products with at most one edge, namely 0 (no edge) and 1 (a single edge), are exactly those of Coxeter order at most 3.

theorem TauCeti.coxeterOrder_eq_two_iff {c : ℤ} (hc : c ∈ {0, 1, 2, 3}) : coxeterOrder c = 2 ↔ c = 0

The product 0 is the only one of Coxeter order 2.

The Coxeter matrix of a generalized Cartan matrix

def TauCeti.coxeterMatrixOfCartanMatrix {B : Type u_1} (A : Matrix B B ℤ) (hdiag : ∀ (i : B), A i i = 2) (hmem : ∀ (i j : B), i ≠ j → A i j * A j i ∈ {0, 1, 2, 3}) : CoxeterMatrix B

The Coxeter matrix read off a Cartan matrix. The entry at a pair of nodes is the Coxeter order TauCeti.coxeterOrder of their Cartan product; on the diagonal that is 1, a node having Cartan product 4 with itself.

Only two properties of the matrix are used, and both are hypotheses here: its diagonal entries are 2, and off the diagonal its Cartan products lie in {0, 1, 2, 3}, the four values that name a dihedral order. It is the construction behind TauCeti.coxeterMatrixOfBase, applied to the Cartan matrix of a base, and behind TauCeti.DynkinType.coxeterMatrix, applied to a standard Cartan matrix in the Bourbaki numbering.

The body is not exposed: TauCeti.coxeterMatrixOfCartanMatrix_apply is the entry API.

Equations

• TauCeti.coxeterMatrixOfCartanMatrix A hdiag hmem = { M := Matrix.of fun (i j : B) => TauCeti.coxeterOrder (A i j * A j i), isSymm := ⋯, diagonal := ⋯, off_diagonal := ⋯ }

@[simp]

theorem TauCeti.coxeterMatrixOfCartanMatrix_apply {B : Type u_1} (A : Matrix B B ℤ) (hdiag : ∀ (i : B), A i i = 2) (hmem : ∀ (i j : B), i ≠ j → A i j * A j i ∈ {0, 1, 2, 3}) (i j : B) : (coxeterMatrixOfCartanMatrix A hdiag hmem).M i j = coxeterOrder (A i j * A j i)

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

theorem TauCeti.coxeterMatrixOfCartanMatrix_apply_eq_two_iff {B : Type u_1} (A : Matrix B B ℤ) (hdiag : ∀ (i : B), A i i = 2) (hmem : ∀ (i j : B), i ≠ j → A i j * A j i ∈ {0, 1, 2, 3}) (hsymm : ∀ (i j : B), A i j = 0 → A j i = 0) {i j : B} (hij : i ≠ j) : (coxeterMatrixOfCartanMatrix A hdiag hmem).M i j = 2 ↔ A i j = 0

Two distinct nodes carry the Coxeter entry 2 exactly when the Cartan entry between them vanishes, provided the zero pattern of the Cartan matrix is symmetric: the product of the two entries then vanishes exactly when the first of them does.

The Cartan product of two simple roots

theorem TauCeti.cartanMatrix_mul_cartanMatrix_eq_coxeterWeightIn {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] (b : P.Base) (i j : ↥b.support) : b.cartanMatrix i j * b.cartanMatrix j i = P.coxeterWeightIn ℤ ↑i ↑j

The Cartan product of a pair of simple roots is their Coxeter weight.

theorem TauCeti.cartanMatrix_mul_cartanMatrix_eq_zero_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] (b : P.Base) [CharZero R] [IsDomain R] (i j : ↥b.support) : b.cartanMatrix i j * b.cartanMatrix j i = 0 ↔ b.cartanMatrix i j = 0

The Cartan product of two simple roots vanishes exactly when the first Cartan entry does: both entries vanish together, since the zero pattern of a Cartan matrix is symmetric.

theorem TauCeti.cartanMatrix_mul_cartanMatrix_eq_zero_iff_isOrthogonal {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] (b : P.Base) [CharZero R] [IsDomain R] (i j : ↥b.support) : b.cartanMatrix i j * b.cartanMatrix j i = 0 ↔ P.IsOrthogonal ↑i ↑j

The Cartan product of two simple roots vanishes exactly when they are orthogonal.

theorem TauCeti.cartanMatrix_mul_cartanMatrix_mem_of_ne {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] {i j : ↥b.support} (hij : i ≠ j) : b.cartanMatrix i j * b.cartanMatrix j i ∈ {0, 1, 2, 3}

The Cartan product of two distinct simple roots lies in {0, 1, 2, 3}, so coxeterOrder reads a genuine Coxeter order off it.

Mathlib confines the Coxeter weight of a finite crystallographic pairing to {0, 1, 2, 3, 4}, and the value 4 is attained only by linearly dependent pairs of roots. Distinct simple roots are linearly independent, which removes it.

theorem TauCeti.cartanMatrix_mul_cartanMatrix_eq_one_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] (b : P.Base) [CharZero R] [IsDomain R] [Finite ι] {i j : ↥b.support} (hij : i ≠ j) : b.cartanMatrix i j * b.cartanMatrix j i = 1 ↔ b.cartanMatrix i j = -1 ∧ b.cartanMatrix j i = -1

The Cartan product of two distinct simple roots is 1 exactly when both Cartan entries are -1, that is, exactly when the two simple roots are joined by a single edge. Off the diagonal the entries are nonpositive, so the alternative factorisation 1 * 1 cannot occur.

The Coxeter matrix of a base

noncomputable def TauCeti.coxeterMatrixOfBase {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) : CoxeterMatrix ↥b.support

The Coxeter matrix of a base. Its entry at a pair of distinct simple roots records the order of the product of the two corresponding simple reflections, read off their Cartan product by 0 ↦ 2, 1 ↦ 3, 2 ↦ 4, 3 ↦ 6; its diagonal entries are 1 because a simple root has Cartan product 4 with itself.

That the entries really are those orders is the classical rank-two computation, and follows in general from the Coxeter presentation of the Weyl group, which is not built here; the entry 2 is checked directly in RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_two_of_coxeterMatrixOfBase_eq_two.

The body is not exposed: TauCeti.coxeterMatrixOfBase_apply is the entry API.

Equations

• TauCeti.coxeterMatrixOfBase P b = TauCeti.coxeterMatrixOfCartanMatrix b.cartanMatrix ⋯ ⋯

@[simp]

theorem TauCeti.coxeterMatrixOfBase_apply {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) (i j : ↥b.support) : (coxeterMatrixOfBase P b).M i j = coxeterOrder (b.cartanMatrix i j * b.cartanMatrix j i)

The entry of the Coxeter matrix of a base at a pair of simple roots is coxeterOrder applied to the product of the two Cartan entries.

theorem TauCeti.coxeterMatrixOfBase_mem_of_ne {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) {i j : ↥b.support} (hij : i ≠ j) : (coxeterMatrixOfBase P b).M i j ∈ {2, 3, 4, 6}

Off the diagonal the Coxeter matrix of a base takes only the four dihedral values.

theorem TauCeti.coxeterMatrixOfBase_ne_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) (i j : ↥b.support) : (coxeterMatrixOfBase P b).M i j ≠ 0

No entry of the Coxeter matrix of a base is infinite: no pair of simple roots of a finite crystallographic root pairing generates an infinite dihedral group.

theorem TauCeti.coxeterMatrixOfBase_le_six {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) (i j : ↥b.support) : (coxeterMatrixOfBase P b).M i j ≤ 6

Every entry of the Coxeter matrix of a base is at most 6, the order attained by the G₂ configuration.

theorem TauCeti.coxeterMatrixOfBase_eq_two_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) (i j : ↥b.support) : (coxeterMatrixOfBase P b).M i j = 2 ↔ P.IsOrthogonal ↑i ↑j

Two simple roots carry the Coxeter entry 2 exactly when they are orthogonal. On the diagonal both sides fail: the entry there is 1, and no root is orthogonal to itself.

theorem TauCeti.isSimplyLaced_iff_forall_coxeterMatrixOfBase_le_three {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) : b.cartanMatrix.IsSimplyLaced ↔ ∀ (i j : ↥b.support), (coxeterMatrixOfBase P b).M i j ≤ 3

The Cartan matrix of a base is simply laced exactly when the Coxeter matrix of that base has all entries at most 3, that is, exactly when no two simple roots are joined by a multiple edge.

The Coxeter entries of the three rank-two Cartan types

theorem TauCeti.coxeterMatrixOfBase_eq_three_of_hasCartanType_A_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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.A 2)) {i j : ↥b.support} (hij : i ≠ j) : (coxeterMatrixOfBase P b).M i j = 3

A base of type A₂ has Coxeter entry 3: the two simple reflections have a product of order 3.

theorem TauCeti.coxeterMatrixOfBase_eq_four_of_hasCartanType_B_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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.B 2)) {i j : ↥b.support} (hij : i ≠ j) : (coxeterMatrixOfBase P b).M i j = 4

A base of type B₂ has Coxeter entry 4.

theorem TauCeti.coxeterMatrixOfBase_eq_six_of_hasCartanType_G2 {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) {i j : ↥b.support} (hij : i ≠ j) : (coxeterMatrixOfBase P b).M i j = 6

A base of type G₂ has Coxeter entry 6: the two simple reflections have a product of order 6, the rotation by a sixth of a turn of the G₂ hexagon.

The orthogonal case: commuting simple reflections

theorem RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_two_of_coxeterMatrixOfBase_eq_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [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) {i j : ↥b.support} (h : (TauCeti.coxeterMatrixOfBase P b).M i j = 2) : orderOf (ofIdx P ↑i * ofIdx P ↑j) = 2

Where the Coxeter matrix of a base has the entry 2, the product of the two simple reflections does have order 2. This is the one entry of coxeterMatrixOfBase that can be checked before the Coxeter presentation of the Weyl group is available.