A base has at most one valid Dynkin type

TauCeti.HasCartanType P b t says that the Cartan matrix of a base b becomes the standard Cartan matrix of the Dynkin type t after one simultaneous relabelling of its rows and columns. This file proves that a base has at most one valid Cartan type: two valid Dynkin types whose standard Cartan matrices are related by such a relabelling are equal. It is the uniqueness half of the Cartan-Killing classification, and it needs no root system at all, only the standard matrices.

Validity is not a convenience here but the content of the statement. Outside the valid ranges the standard matrices genuinely repeat: B 1 and C 1 are A 1, D 3 is A 3 after a relabelling (CartanMatrix.D_three'), and C 2 is B 2 with its two nodes exchanged. Uniqueness therefore has to fail without TauCeti.DynkinType.Valid, and every use of validity below is at one of those coincidences.

The invariants

A relabelling preserves the size of a matrix, and it preserves any property phrased in terms of entries and row sums alone. Four such properties separate the nine valid families, and computing their values on the standard matrices is the arithmetic content of the file.

For a simply-laced type the row sum ∑ j, A i j is 2 minus the degree of the node i, so the value -1 marks a node of degree three, a branch node, and the value 1 marks a node of degree one, a leaf. That reading is what the names below record, but no graph is ever formed: the row sum is used as it stands, which is also why the same invariant is legitimate for the multiply-laced types, where the degree reading fails (F₄ has a row summing to -1 and no branch node).

• a multiple edge, an off-diagonal entry ≤ -2: this holds for exactly the non-simply-laced valid types B, C, F₄, G₂;
• a double edge at a leaf, a node whose row sums to 1 and whose column contains an entry -2: this holds for exactly B, and is what separates Bₙ from its transpose Cₙ and from F₄, whose double edge is interior;
• a row summing to -1: this holds for D, E₆, E₇, E₈, F₄, G₂, and fails for A and C;
• a branch node with two leaves, a row summing to -1 with at least two nonzero entries in columns summing to 1: this holds for Dₙ and fails for E₆, E₇, E₈, which is the one separation the rank does not already make.

Main results

• TauCeti.DynkinType.eq_of_valid_of_cartanMatrix_eq: two valid Dynkin types whose standard Cartan matrices agree up to a simultaneous relabelling are equal.
• TauCeti.DynkinType.eq_of_valid_of_forall_eq: the same statement for a matrix carrying two such relabellings, which is the form the classification theorems consume.
• TauCeti.HasCartanType.eq_of_valid: a base has at most one valid Cartan type.
• TauCeti.HasCartanType.existsUnique_of_valid: a base of some valid Cartan type has exactly one.

References

This is the uniqueness half of existsUnique_dynkinType, the classification target of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md; the existence half, which produces a valid type in the first place, is independent of it. The coincidences outside the valid ranges are those of Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI, §4.

The invariants of the standard Cartan matrices

The classical families need their row sums computed by hand. Each row of a classical Cartan matrix has at most four nonzero entries, so the row is rewritten as a sum of that many indicator functions of a column index and summed term by term. The exceptional matrices are finite data, so decide reads their invariants off directly.

theorem TauCeti.DynkinType.eq_of_valid_of_cartanMatrix_eq {t t' : DynkinType} (ht : t.Valid) (ht' : t'.Valid) (e : Fin t.rank ≃ Fin t'.rank) (he : ∀ (i j : Fin t.rank), t.cartanMatrix i j = t'.cartanMatrix (e i) (e j)) : t = t'

The Dynkin type of a Cartan matrix is unique among valid types. If the standard Cartan matrices of two valid Dynkin types agree after one simultaneous relabelling of rows and columns, the two types are equal.

Validity is necessary rather than convenient: CartanMatrix.D_three' relabels D 3 to A 3, and B 1 and C 1 are A 1, so the statement fails for types outside their valid ranges.

theorem TauCeti.DynkinType.eq_of_valid_of_forall_eq {α : Type u_1} {A : Matrix α α ℤ} {t t' : DynkinType} (ht : t.Valid) (ht' : t'.Valid) (e : α ≃ Fin t.rank) (e' : α ≃ Fin t'.rank) (he : ∀ (i j : α), A i j = t.cartanMatrix (e i) (e j)) (he' : ∀ (i j : α), A i j = t'.cartanMatrix (e' i) (e' j)) : t = t'

A matrix has at most one valid Dynkin type. If a matrix agrees entrywise with the standard Cartan matrices of two valid Dynkin types, each under its own relabelling of the index type, the two types are equal. This is the form the classification theorems consume, their statements being ∃! t, t.Valid ∧ ∃ e : α ≃ Fin t.rank, ∀ i j, A i j = t.cartanMatrix (e i) (e j).

theorem TauCeti.HasCartanType.eq_of_valid {ι : 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] {b : P.Base} {t t' : DynkinType} (h : HasCartanType P b t) (h' : HasCartanType P b t') (ht : t.Valid) (ht' : t'.Valid) : t = t'

A base has at most one valid Cartan type. This is the uniqueness half of the Cartan-Killing classification; producing a valid type in the first place is the independent existence half.

theorem TauCeti.HasCartanType.existsUnique_of_valid {ι : 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] {b : P.Base} {t : DynkinType} (h : HasCartanType P b t) (ht : t.Valid) : ∃! s : DynkinType, s.Valid ∧ HasCartanType P b s

A base of some valid Cartan type has exactly one.