Cartan matrices of finite type

The Cartan-Killing classification is, at bottom, a statement about integer matrices: the Cartan matrix of a finite crystallographic root system is a generalized Cartan matrix that is symmetrizable with positive definite symmetrization, and only finitely many combinatorial shapes of such a matrix exist. This file introduces the matrix-level condition, Ado.IsFiniteType, develops the tools that eliminate diagrams from the list, and proves that the Cartan matrix of a base of a finite crystallographic root system satisfies it.

Positive definiteness is asked for over ℚ, not over ℤ. Ado.Matrix.posDef_map_intCast shows that positive definiteness over ℤ implies positive definiteness over ℚ, and the rational form is the one downstream arguments use, since a test vector produced by a diagram computation need not have integer entries. The symmetrizer d is likewise rational: it is the vector of inverse root lengths, which is integral only after clearing denominators. The symmetrization itself is not redone here: Mathlib packages it over ℤ as RootPairing.Base.exists_cartanMatrix_diagaonal_mul_posDef, resting on RootPairing.posRootForm_rootFormIn_posDef.

Main definitions

• Ado.IsFiniteType: an integer matrix is a generalized Cartan matrix admitting a positive rational symmetrizer whose symmetrization is positive definite.

Main results

• Ado.isFiniteType_of: a constructor that does not ask for the symmetric vanishing pattern, which the symmetrizer already forces.
• Ado.isFiniteType_of_posDef_map_intCast: the constructor for a generalized Cartan matrix whose rational cast is itself positive definite, with the constant-one symmetrizer. The simply-laced Cartan matrices are of this kind.
• Ado.isFiniteType_of_conjTranspose_mul_self_of_det_ne_zero: the constructor used for a matrix presented by its entries. Positive definiteness of the symmetrization is certified by an explicit Gram model Cᴴ * C together with nonsingularity, both of which are finite computations.
• Ado.IsFiniteType.submatrix: principal submatrices of a finite-type matrix are of finite type. This is what lets a forbidden subdiagram rule out a diagram containing it.
• Ado.IsFiniteType.transpose: finite type is invariant under matrix transposition.
• Ado.IsFiniteType.sum_apply_mul_apply_lt_four: the star bound. The Cartan products joining an index to pairwise non-adjacent neighbours sum to less than 4. This is the first of the two positive-definiteness estimates behind the local shape of a finite-type diagram.
• Ado.IsFiniteType.apply_mul_apply_mem_of_ne: the rank-two bound. For i ≠ j the Cartan product A i j * A j i lies in {0, 1, 2, 3}, so every edge of the diagram is single, double or triple.
• Ado.IsFiniteType.isSimplyLaced_iff: a finite-type matrix is simply laced exactly when none of its edges is multiple, that is, when no Cartan product of two distinct indices exceeds 1. Together with the rank-two bound this is how the classification enters its simply-laced branch, having excluded the Cartan products 2 and 3.
• Ado.IsFiniteType.exists_apply_succ_eq_zero: a finite-type diagram carries no cycle. A cyclic list of at least three distinct indices has a missing edge. This is the second estimate: the test vector is supported on the indices of the putative cycle, its coordinate at each of them being the reciprocal of the symmetrizer, and each edge of the cycle then cancels the diagonal contribution of one of its ends.
• Ado.IsFiniteType.apply_eq_zero_of_apply_ne_zero: a finite-type diagram carries no triangle, the three-index case of the previous item: two distinct neighbours of an index are never adjacent to one another. Ado.IsFiniteType.pairwise_apply_eq_zero is the same statement for a whole neighbourhood, in the shape the star bound consumes.

The star bound selects its neighbours through a pairwise non-adjacency hypothesis; with the triangle excluded that hypothesis comes for free, and the consequences below are the unconditional graph statements the classification runs on.

• Ado.IsFiniteType.card_le_three_of_forall_apply_ne_zero: the degree bound. No index has four neighbours; the affine type D4 is ruled out in Ado.not_isFiniteType_affineD₄.
• Ado.IsFiniteType.apply_mul_apply_le_one_of_two_le: at most one edge at an index is multiple.
• Ado.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three: a triple edge is isolated, so it is a connected component of the diagram; this is why G₂ has rank 2.
• Ado.IsFiniteType.apply_mul_apply_eq_one_of_three_le_card: a branch vertex is simply laced. Three neighbours of an index are each joined to it by a single edge.
• Ado.IsFiniteType.det_ne_zero: a finite-type matrix is nonsingular. Since the extended Dynkin diagrams have singular Cartan matrices, this is the third elimination tool; the affine type Ã₂ is ruled out in Ado.not_isFiniteType_affineA₂. It does not subsume the no-triangle theorem: Ado.not_isFiniteType_doubleEdgeTriangle exhibits a nonsingular triangle.
• Ado.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos: a finite-type matrix has no nonzero subdominant vector, one with xᵢ · (A x)ᵢ ≤ 0 at every index. This is the fourth elimination tool, and unlike Ado.IsFiniteType.det_ne_zero it does not ask the certificate to be a null vector, only to point away from the positive cone coordinatewise, so a single vector can rule out a whole family of diagrams.
• Ado.isFiniteType_cartanMatrix: the Cartan matrix of a base of a finite crystallographic root system is of finite type, and Ado.HasCartanType.isFiniteType: so is the standard Cartan matrix of any Dynkin type realized by such a base.

References

This file implements the "finite-type condition" item of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signature isFiniteType_cartanMatrix in that roadmap's Suggested.lean. See V. G. Kac, Infinite Dimensional Lie Algebras, 3rd ed., Chapter 4, for the finite/affine/indefinite trichotomy of generalized Cartan matrices, and Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter 11, for the classification of the finite-type case.

def Ado.IsFiniteType {B : Type u_1} (A : Matrix B B ℤ) : Prop

A finite square integer matrix is of finite type when it is a generalized Cartan matrix - diagonal entries 2, nonpositive off-diagonal entries, and a symmetric vanishing pattern - which is symmetrizable with positive definite symmetrization: there is a positive rational vector d making fun i j ↦ d i * A i j positive definite (in particular symmetric).

The Cartan matrices of finite root systems are exactly the matrices of this kind, up to irreducibility; Ado.isFiniteType_cartanMatrix proves one direction.

Equations

• One or more equations did not get rendered due to their size.

theorem Ado.isFiniteType_of {B : Type u_1} {A : Matrix B B ℤ} (h2 : ∀ (i : B), A i i = 2) (hle : ∀ (i j : B), i ≠ j → A i j ≤ 0) {d : B → ℚ} (hd : ∀ (i : B), 0 < d i) (hpd : (Matrix.of fun (i j : B) => d i * ↑(A i j)).PosDef) : IsFiniteType A

Building a finite-type matrix. The symmetric vanishing pattern demanded by Ado.IsFiniteType need not be checked: a positive symmetrizer already forces d j * A j i = d i * A i j, so one entry of a transposed pair vanishes exactly when the other does. The clause is kept in the definition because it is one of the defining axioms of a generalized Cartan matrix.

theorem Ado.isFiniteType_of_posDef_map_intCast {B : Type u_1} {A : Matrix B B ℤ} (h2 : ∀ (i : B), A i i = 2) (hle : ∀ (i j : B), i ≠ j → A i j ≤ 0) (hpd : (A.map Int.cast).PosDef) : IsFiniteType A

A generalized Cartan matrix that is positive definite over ℚ is of finite type. The symmetrizer is the constant-one vector, whose symmetrization of A is A itself read over ℚ; so the diagonal and sign conditions of Ado.isFiniteType_of are still required, and only the symmetrizer is fixed. This is the constructor for the simply-laced Cartan matrices, which are symmetric and are the Gram matrices of their own simple roots.

theorem Ado.isFiniteType_of_conjTranspose_mul_self_of_det_ne_zero {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] [DecidableEq B] {m : Type u_2} [Fintype m] (h2 : ∀ (i : B), A i i = 2) (hle : ∀ (i j : B), i ≠ j → A i j ≤ 0) {d : B → ℚ} (hd : ∀ (i : B), 0 < d i) {C : Matrix m B ℚ} (hgram : (Matrix.of fun (i j : B) => d i * ↑(A i j)) = C.conjTranspose * C) (hdet : A.det ≠ 0) : IsFiniteType A

A nonsingular generalized Cartan matrix with a rational Gram model is of finite type. This is the working form of Ado.isFiniteType_of for a matrix given by an explicit list of entries: positive definiteness of the symmetrization is certified by exhibiting it as Cᴴ * C for a matrix C of coordinates - the columns of C being simple coroots, in the intended application - which makes it positive semidefinite, with nonsingularity of A upgrading that to positive definiteness.

theorem Ado.IsFiniteType.apply_self {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (i : B) : A i i = 2

The diagonal entries of a finite-type matrix are 2.

theorem Ado.IsFiniteType.apply_le_zero_of_ne {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {i j : B} (hij : i ≠ j) : A i j ≤ 0

The off-diagonal entries of a finite-type matrix are nonpositive.

theorem Ado.IsFiniteType.apply_eq_zero_symm {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {i j : B} (hij : A i j = 0) : A j i = 0

The vanishing pattern of a finite-type matrix is symmetric.

theorem Ado.IsFiniteType.apply_eq_zero_iff {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {i j : B} : A i j = 0 ↔ A j i = 0

An entry of a finite-type matrix vanishes exactly when its transpose does.

theorem Ado.IsFiniteType.exists_symmetrizer {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) : ∃ (d : B → ℚ), (∀ (i : B), 0 < d i) ∧ (Matrix.of fun (i j : B) => d i * ↑(A i j)).PosDef

The symmetrizer of a finite-type matrix, together with its defining properties.

theorem Ado.IsFiniteType.submatrix {B : Type u_1} {A : Matrix B B ℤ} {C : Type u_2} (h : IsFiniteType A) {e : C → B} (he : Function.Injective e) : IsFiniteType (A.submatrix e e)

A principal submatrix of a finite-type matrix is of finite type. This is the form in which a forbidden subdiagram excludes every diagram containing it.

theorem Ado.IsFiniteType.transpose {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) : IsFiniteType A.transpose

Finite type is invariant under transposition. The reciprocal vector is a symmetrizer for the transpose. Its symmetrization is obtained from the original one by conjugating with the invertible diagonal matrix whose entries are those reciprocals.

theorem Ado.IsFiniteType.one_le_apply_mul_apply {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {i j : B} (hne : A i j ≠ 0) : 1 ≤ A i j * A j i

A nonzero entry has Cartan product at least 1. Off the diagonal both entries of such a transposed pair are at most -1: they are nonpositive, and neither vanishes, because the vanishing pattern is symmetric. On the diagonal the product is 2 * 2.

theorem Ado.IsFiniteType.sum_apply_mul_apply_lt_four {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i : B} {s : Finset B} (his : i ∉ s) (hs : (↑s).Pairwise fun (j k : B) => A j k = 0) : ∑ j ∈ s, A i j * A j i < 4

The star bound. If i is distinct from every index of s and the indices of s are pairwise non-adjacent, then the Cartan products of i with the indices of s sum to less than 4.

This is the first of the two positive-definiteness estimates behind the local shape of a finite-type diagram: inside a pairwise non-adjacent star at i there are at most three neighbours, at most one of the edges to them is multiple, and a triple edge among them stands alone. The second, Ado.IsFiniteType.apply_eq_zero_of_apply_ne_zero, removes the pairwise hypothesis.

theorem Ado.IsFiniteType.apply_mul_apply_mem_of_ne {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i j : B} (hij : i ≠ j) : A i j * A j i ∈ {0, 1, 2, 3}

The Cartan product of two distinct indices of a finite-type matrix is 0, 1, 2 or 3. These are exactly the values that name the orders 2, 3, 4, 6 of a product of two simple reflections.

theorem Ado.IsFiniteType.isSimplyLaced_iff {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) : A.IsSimplyLaced ↔ ∀ (i j : B), i ≠ j → A i j * A j i ≤ 1

A finite-type matrix is simply laced exactly when none of its edges is multiple. The Cartan product A i j * A j i is the multiplicity of the edge joining i and j, so the condition on the right says that every edge is single: no double edge, and no triple edge.

Only the off-diagonal entries are constrained, one entry of a transposed pair at a time, and that is enough because the entries of such a pair vanish together and a product of two nonpositive integers is 1 only when both are -1.

theorem Ado.IsFiniteType.exists_apply_succ_eq_zero {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {m : ℕ} [NeZero m] (hm : 3 ≤ m) {v : Fin m → B} (hv : Function.Injective v) : ∃ (k : Fin m), A (v k) (v (k + 1)) = 0

A finite-type diagram carries no cycle. A cyclic list of at least three distinct indices has a missing edge: some index of the cycle is not joined to its successor. The cycle is not required to be chordless, and no edge of it is required to be simple.

Only the principal submatrix on the indices of the cycle is involved, so this is Ado.IsFiniteType.exists_apply_succ_eq_zero_fin transported along the injection. Ado.IsFiniteType.isAcyclic_diagramGraph is the same statement in the language of graphs.

theorem Ado.IsFiniteType.apply_eq_zero_of_apply_ne_zero {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {i j k : B} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hj : A i j ≠ 0) (hk : A i k ≠ 0) : A j k = 0

A finite-type diagram carries no triangle. Two distinct neighbours of an index are never adjacent to one another, so the neighbourhood of an index is pairwise non-adjacent and the star bound applies to it with no side condition.

This is the three-index case of Ado.IsFiniteType.exists_apply_succ_eq_zero, and it is what turns the conditional consequences of the star bound into graph statements: the degree bound Ado.IsFiniteType.card_le_three_of_forall_apply_ne_zero, the fact that at most one edge at an index is multiple, and the isolation of a triple edge.

theorem Ado.IsFiniteType.pairwise_apply_eq_zero {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {i : B} {s : Finset B} (his : i ∉ s) (hadj : ∀ j ∈ s, A i j ≠ 0) : (↑s).Pairwise fun (j k : B) => A j k = 0

The neighbourhood of an index is pairwise non-adjacent. This is the no-triangle theorem in the form the star bound consumes: a set of neighbours of i, none of them i itself, satisfies the pairwise hypothesis of Ado.IsFiniteType.sum_apply_mul_apply_lt_four for free.

theorem Ado.IsFiniteType.apply_mul_apply_add_apply_mul_apply_lt_four {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i j k : B} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : A i j * A j i + A i k * A k i < 4

The two-index case of the star bound. Three pairwise distinct indices i, j, k are such that the Cartan products of i with j and with k sum to less than 4; neither j nor k is required to be a neighbour of i, an absent edge contributing 0. No non-adjacency of j and k is assumed: if both are neighbours of i the no-triangle theorem supplies it, and otherwise the rank-two bound alone already caps the sum at 3.

theorem Ado.IsFiniteType.apply_mul_apply_le_one_of_two_le {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i j k : B} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hj : 2 ≤ A i j * A j i) : A i k * A k i ≤ 1

At most one edge at an index is multiple. An index carrying a multiple edge to j is joined to every index other than j by at most a single edge. No non-adjacency of the far ends is assumed: the no-triangle theorem supplies it.

theorem Ado.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i j k : B} (hik : i ≠ k) (hjk : j ≠ k) (hj : A i j * A j i = 3) : A i k = 0

A triple edge is isolated. An index joined to j by a triple edge is joined to no index other than j at all; applied at both ends of the edge this says that a triple edge is a connected component of the diagram, which is why G₂ has rank 2. Here i ≠ j need not be assumed: it follows from the Cartan product being 3 rather than the diagonal value 4.

theorem Ado.IsFiniteType.card_le_three_of_forall_apply_ne_zero {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i : B} {s : Finset B} (his : i ∉ s) (hadj : ∀ j ∈ s, A i j ≠ 0) : s.card ≤ 3

The degree bound: an index of a finite-type matrix has at most three neighbours, so a finite-type diagram branches into at most three arms. By the no-triangle theorem the neighbours are automatically pairwise non-adjacent, so the star bound applies to them directly.

theorem Ado.IsFiniteType.apply_mul_apply_eq_one_of_three_le_card {B : Type u_1} {A : Matrix B B ℤ} [Finite B] (h : IsFiniteType A) {i : B} {s : Finset B} (his : i ∉ s) (hadj : ∀ j ∈ s, A i j ≠ 0) (hcard : 3 ≤ s.card) {j : B} (hj : j ∈ s) : A i j * A j i = 1

A three-armed star of a finite-type matrix is simply laced. An index with three neighbours meets each of them along a single edge, since three Cartan products of value at least 1 already exhaust the star bound. Together with Ado.IsFiniteType.card_le_three_of_forall_apply_ne_zero this says that a branch vertex of a finite-type diagram carries exactly three simple edges.

theorem Ado.IsFiniteType.det_ne_zero {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] [DecidableEq B] (h : IsFiniteType A) : A.det ≠ 0

A finite-type matrix is nonsingular. This is the elimination tool for the extended Dynkin diagrams, whose Cartan matrices are singular.

theorem Ado.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) {x : B → ℚ} (hx : ∀ (i : B), x i * ∑ j : B, ↑(A i j) * x j ≤ 0) : x = 0

A finite-type matrix admits no nonzero subdominant vector. Call a rational vector x subdominant for A when xᵢ · (A x)ᵢ ≤ 0 at every index i; then x = 0.

The symmetrized quadratic form of A at x is ∑ᵢ dᵢ · xᵢ · (A x)ᵢ, because scaling the i-th row by dᵢ scales the i-th summand by dᵢ, and the symmetrizer is positive. So a subdominant vector makes the form nonpositive, which positive definiteness allows only at 0.

This is the elimination tool for a diagram carrying an explicit certificate. It is weaker than asking for a null vector, as Ado.IsFiniteType.det_ne_zero does: the certificate is allowed to be strictly subdominant at some indices, which is what lets a single vector rule out a whole family of diagrams rather than only the critical ones.

theorem Ado.not_isFiniteType_affineA₂ : ¬IsFiniteType !![2, -1, -1; -1, 2, -1; -1, -1, 2]

The Cartan matrix of the affine diagram Ã₂ is not of finite type. The three-cycle is a genuine generalized Cartan matrix, symmetric with every Cartan product equal to 1, so neither the combinatorial axioms nor the rank-two bound exclude it; it is positive semidefinite. The proof below rules it out by Ado.IsFiniteType.det_ne_zero, which is merely the tool it uses: being a triangle, Ã₂ is excluded by Ado.IsFiniteType.apply_eq_zero_of_apply_ne_zero as well, and it is exactly the equality case of that estimate.

theorem Ado.not_isFiniteType_affineD₄ : ¬IsFiniteType !![2, -1, -1, -1, -1; -1, 2, 0, 0, 0; -1, 0, 2, 0, 0; -1, 0, 0, 2, 0; -1, 0, 0, 0, 2]

The Cartan matrix of the affine diagram D4 is not of finite type. The four-armed star is the smallest diagram excluded by the degree bound; unlike Ã₂ it needs no determinant, since Ado.IsFiniteType.card_le_three_of_forall_apply_ne_zero applies to the central index directly.

theorem Ado.not_isFiniteType_doubleEdgeTriangle : ¬IsFiniteType !![2, -2, -1; -1, 2, -1; -1, -2, 2]

A triangle carrying double edges is not of finite type. This matrix is a generalized Cartan matrix; it is symmetrizable, by d = (1, 2, 1); its Cartan products 2, 1, 2 all lie in the rank-two range; and it is nonsingular, with determinant -6. So neither the combinatorial axioms, nor Ado.IsFiniteType.apply_mul_apply_mem_of_ne, nor Ado.IsFiniteType.det_ne_zero excludes it. Neither does the star bound: no two of the three indices are non-adjacent, so the only neighbour sets meeting its pairwise non-adjacency hypothesis are the empty and the singleton ones, whose Cartan products sum to at most 2 and so stay clear of the bound. It is Ado.IsFiniteType.apply_eq_zero_of_apply_ne_zero that rules it out.

theorem Ado.isFiniteType_cartanMatrix {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] (b : P.Base) : IsFiniteType b.cartanMatrix

The Cartan matrix of a base of a finite crystallographic root system is of finite type. The symmetrizer is the vector of inverse root lengths for the canonical form.

Reducedness is not assumed: positive definiteness of the canonical form does not need it.

theorem Ado.HasCartanType.isFiniteType {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] {b : P.Base} {t : DynkinType} (h : HasCartanType P b t) : IsFiniteType t.cartanMatrix

The standard Cartan matrix of a Dynkin type realized by a base is of finite type. This is the shape in which the finite-type condition eliminates candidate Dynkin types.