The Cartan-Killing classification in rank at most two

The classification of finite-type Cartan matrices proceeds by induction on the number of nodes, and its base cases are the diagrams with one and with two nodes. This file settles them: an indecomposable finite-type matrix on two indices is, after a single simultaneous relabelling of its rows and columns, exactly one of the three standard rank-two Cartan matrices A₂, B₂, G₂, and on one index it is A₁.

Producing the type turns on one invariant. The Cartan product AᵢⱼAⱼᵢ of the two nodes is unchanged by relabelling, is at least 1 because the diagram is connected, and is at most 3 because the matrix is of finite type (TauCeti.IsFiniteType.apply_mul_apply_mem_of_ne). Its three possible values 1, 2, 3 separate the three types, and each value pins the pair of off-diagonal entries to (-1, -1), to (-1, -2) and to (-1, -3) respectively. What is left to the relabelling is then only the orientation of the multiple edge, which is what TauCeti.HasCartanType records and why the equivalence produced below is not always the one the ambient indexing suggests. That the type so produced is the only valid one is not proved here: it is TauCeti.DynkinType.eq_of_valid_of_forall_eq, which says that of any rank.

Two remarks on what the statements say. First, C 2 is absent from the list, and must be: it is the transpose of B 2 and names the same root system, so TauCeti.DynkinType.Valid keeps only the name B 2 (see TauCeti.hasCartanType_dual_iff_of_rank_le_two). Uniqueness of the type would be false without that exclusion. Second, connectedness is a genuine hypothesis at the matrix level, and is supplied by irreducibility at the root-system level through TauCeti.cartanMatrix_ne_zero_of_card_support_eq_two: a matrix whose two nodes are orthogonal is the Cartan matrix of A₁ × A₁, of finite type but not irreducible.

Main results

• TauCeti.DynkinType.valid_and_rank_eq_two_iff: the valid Dynkin types of rank two are exactly A 2, B 2 and G2.
• TauCeti.IsFiniteType.existsUnique_dynkinType_of_card_eq_two: an indecomposable finite-type matrix on two indices has exactly one valid Dynkin type.
• TauCeti.cartanMatrix_ne_zero_of_card_support_eq_two: the Cartan matrix of a base of an irreducible reduced pairing with two simple roots has no off-diagonal zero entry.
• TauCeti.existsUnique_dynkinType_of_card_support_eq_two: an irreducible reduced crystallographic finite root system with two simple roots is of exactly one of the types A₂, B₂, G₂; TauCeti.hasCartanType_of_card_support_eq_two is the same statement as a three-way disjunction.
• TauCeti.isG2_of_hasCartanType_G2: a base of type G₂ makes its pairing Mathlib's RootPairing.IsG2.
• TauCeti.hasCartanType_G2_of_isG2: conversely, a base of an IsG2 pairing is of type G₂, so the two conditions agree (TauCeti.hasCartanType_G2_iff_isG2). This is the direction that needs the roots away from the base, and it closes the recognition step that Mathlib's G₂ file lists as a TODO.
• TauCeti.existsUnique_dynkinType_of_card_support_eq_one: the rank-one case, which turns on the diagonal entry 2 alone and so needs neither finiteness, finite type nor irreducibility.

References

This file supplies the rank-one and rank-two cases of the Layer 5 milestone "the classification of finite-type Cartan matrices" of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, whose statement existsUnique_dynkinType these theorems specialize. See Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4, and Humphreys, Introduction to Lie Algebras and Representation Theory, §11.1, where the rank-two diagrams are enumerated first for exactly this reason.

@[simp]

theorem TauCeti.DynkinType.valid_and_rank_eq_two_iff {t : DynkinType} : t.Valid ∧ t.rank = 2 ↔ t = A 2 ∨ t = B 2 ∨ t = G2

The valid Dynkin types of rank two are A₂, B₂ and G₂. The type C 2 is excluded by TauCeti.DynkinType.Valid, being B 2 transposed; every other type either has a different rank or fails validity at rank two.

theorem TauCeti.DynkinType.cartanMatrix_A_two_eq : (A 2).cartanMatrix = !![2, -1; -1, 2]

The standard Cartan matrix of type A₂.

theorem TauCeti.DynkinType.cartanMatrix_B_two_eq : (B 2).cartanMatrix = !![2, -2; -1, 2]

The standard Cartan matrix of type B₂: the arrow of the double edge runs from the long simple root at Bourbaki node 1 to the short simple root at node 2.

theorem TauCeti.DynkinType.cartanMatrix_G2_eq : G2.cartanMatrix = !![2, -1; -3, 2]

The standard Cartan matrix of type G₂ in the Bourbaki numbering, node 1 short and node 2 long.

The classification of matrices on at most two indices

theorem TauCeti.Matrix.mul_apply_mul_apply_eq_of_equiv_fin_two {B : Type u_1} {A : Matrix B B ℤ} {C : Matrix (Fin 2) (Fin 2) ℤ} (e : B ≃ Fin 2) (he : ∀ (i j : B), A i j = C (e i) (e j)) {x y : B} (hxy : x ≠ y) : A x y * A y x = C 0 1 * C 1 0

The Cartan product is the invariant of a two-node diagram. A relabelling matching A with C carries the product of the two off-diagonal entries of A to that of C, whichever way round it sends the two indices, because the product is symmetric.

theorem TauCeti.IsFiniteType.existsUnique_dynkinType_of_card_eq_two {B : Type u_1} [Fintype B] {A : Matrix B B ℤ} (h : IsFiniteType A) (hcard : Fintype.card B = 2) (hconn : ∀ (i j : B), i ≠ j → A i j ≠ 0) : ∃! t : DynkinType, t.Valid ∧ ∃ (e : B ≃ Fin t.rank), ∀ (i j : B), A i j = t.cartanMatrix (e i) (e j)

The rank-two classification of finite-type matrices. A finite-type matrix on two indices whose off-diagonal entries are nonzero — that is, whose diagram is connected — has exactly one valid Dynkin type: it is A₂, B₂ or G₂ according as the Cartan product of its two nodes is 1, 2 or 3.

theorem TauCeti.existsUnique_dynkinType_of_card_eq_one {B : Type u_1} [Fintype B] {A : Matrix B B ℤ} (hdiag : ∀ (i : B), A i i = 2) (hcard : Fintype.card B = 1) : ∃! t : DynkinType, t.Valid ∧ ∃ (e : B ≃ Fin t.rank), ∀ (i j : B), A i j = t.cartanMatrix (e i) (e j)

A matrix on one index with diagonal entry 2 is A₁. Only that entry is in play, so the hypothesis is the diagonal equation itself rather than TauCeti.IsFiniteType: neither the finite-type inequalities nor connectedness are used.

The classification of root systems of rank at most two

theorem TauCeti.cartanMatrix_ne_zero_of_card_support_eq_two {ι : 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} [P.IsCrystallographic] [Finite ι] [CharZero R] [IsDomain R] [P.IsReduced] [P.IsIrreducible] (b : P.Base) (hb : b.support.card = 2) {i j : ↥b.support} (hij : i ≠ j) : b.cartanMatrix i j ≠ 0

A rank-two irreducible diagram is connected. With only two simple roots, irreducibility leaves no room for the diagram to split: the single off-diagonal pair of Cartan entries cannot vanish. This is the hypothesis that TauCeti.IsFiniteType.existsUnique_dynkinType_of_card_eq_two asks for, and the reason A₁ × A₁ is not a counterexample to the classification.

theorem TauCeti.existsUnique_dynkinType_of_card_support_eq_two {ι : 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} [P.IsCrystallographic] [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsReduced] [P.IsIrreducible] (b : P.Base) (hb : b.support.card = 2) : ∃! t : DynkinType, t.Valid ∧ HasCartanType P b t

A root system with two simple roots is of type A₂, B₂ or G₂, and of exactly one of them. This is the rank-two case of the Cartan-Killing classification: existence and uniqueness of a valid Dynkin type for an irreducible reduced crystallographic finite root system.

theorem TauCeti.hasCartanType_of_card_support_eq_two {ι : 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} [P.IsCrystallographic] [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsReduced] [P.IsIrreducible] (b : P.Base) (hb : b.support.card = 2) : HasCartanType P b (DynkinType.A 2) ∨ HasCartanType P b (DynkinType.B 2) ∨ HasCartanType P b DynkinType.G2

The rank-two classification, as a three-way disjunction.

theorem TauCeti.isG2_of_hasCartanType_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} [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] {b : P.Base} (h : HasCartanType P b DynkinType.G2) : P.IsG2

A base of Cartan type G₂ makes its root pairing Mathlib's RootPairing.IsG2. The entry -3 of the standard G₂ Cartan matrix is the pairing of two simple roots, which is exactly the datum RootPairing.IsG2 asks for; RootPairing.IsG2.card_base_support_eq_two is the matching fact that an IsG2 pairing has a rank-two base. TauCeti.hasCartanType_G2_of_isG2 is the converse, and needs more: excluding type A₂ turns on the pairings of all roots, not only the simple ones.

theorem TauCeti.hasCartanType_G2_of_isG2 {ι : 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} [P.IsCrystallographic] [Finite ι] [CharZero R] [IsDomain R] (hG2 : P.IsG2) (b : P.Base) : HasCartanType P b DynkinType.G2

An IsG2 root pairing has Cartan type G₂. This is the converse of TauCeti.isG2_of_hasCartanType_G2, and it is the harder direction, because RootPairing.IsG2 asks only that some pair of roots pair to -3, while the conclusion is about the two simple roots of the given base.

The bridge is root length. A pair of roots pairing to -3 has its transposed pairing -1, so the two differ in squared length by the factor 3; every root has the length of a simple root (RootPairing.RootPositiveForm.exists_mem_support_rootLength_eq), so two of the simple roots already differ by that factor, and reading the ratio back off the Cartan matrix makes their two off-diagonal entries -3 and -1. Since the base has two elements, these entries and the diagonal entries 2 identify its Cartan matrix with the standard matrix of G₂.

@[simp]

theorem TauCeti.hasCartanType_G2_iff_isG2 {ι : 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} [P.IsCrystallographic] [Finite ι] [CharZero R] [IsDomain R] [P.IsReduced] [P.IsIrreducible] (b : P.Base) : HasCartanType P b DynkinType.G2 ↔ P.IsG2

Cartan type G₂ and Mathlib's RootPairing.IsG2 are the same condition. The right-hand side does not mention the base, so an irreducible reduced crystallographic finite root pairing with one base of type G₂ has every base of type G₂. The IsG2 hypothesis of TauCeti.hasCartanType_G2_of_isG2 is taken as an argument rather than as an instance, so that it can be supplied by the right-hand side here.

theorem TauCeti.existsUnique_dynkinType_of_card_support_eq_one {ι : 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} [P.IsCrystallographic] [CharZero R] (b : P.Base) (hb : b.support.card = 1) : ∃! t : DynkinType, t.Valid ∧ HasCartanType P b t

A pairing with a single simple root is of type A₁. Neither finiteness nor irreducibility is needed, nor even that the pairing is a root system: the Cartan matrix is the 1 × 1 matrix [2] by RootPairing.Base.cartanMatrix_apply_same, which is all the rank-one classification consumes.