Affine type D̃ₘ for m ≥ 5 is not of finite type

The diagram of an indecomposable finite-type Cartan matrix is a tree of maximum degree three. To finish the simply-laced part of the Cartan--Killing classification one must also show that such a tree cannot have two branch vertices. The path between two branch vertices, together with two branches at either end, contains an affine diagram of type D. This file supplies the uniform matrix obstruction for that argument.

The matrix doubleForkCartanMatrix n has two fork vertices joined by a chain with n internal vertices. Each fork vertex has two leaves. Thus it is the affine diagram D̃ₘ for m = n + 5, so this construction covers exactly the family D̃ₘ for m ≥ 5. The vector which is 1 on the four leaves and 2 on the middle chain is a nonzero null vector. Since a finite-type matrix has positive-definite symmetrization, it cannot admit this vector.

The spine of the diagram is a chain, so its entries and the row sum along it come from TauCeti.LinearAlgebra.RootSystem.Chain, which the star obstructions of TauCeti.LinearAlgebra.RootSystem.FiniteType.Star share.

Main definitions

• TauCeti.DoubleForkIndex: the four leaves and the vertices of the middle chain.
• TauCeti.doubleForkCartanMatrix: the simply-laced double-fork Cartan matrix.
• TauCeti.doubleForkMark: the affine marks, equal to 1 on leaves and 2 on the chain.

Main results

• TauCeti.sum_doubleForkCartanMatrix_mul_doubleForkMark_eq_zero and TauCeti.doubleForkCartanMatrix_mulVec_doubleForkMark_eq_zero: the affine marks form a null vector, row by row and as a matrix-vector product.
• TauCeti.doubleForkCartanMatrix_diag, TauCeti.isSimplyLaced_doubleForkCartanMatrix, TauCeti.doubleForkCartanMatrix_off_diag_nonpos, TauCeti.doubleForkCartanMatrix_isSymm and TauCeti.doubleForkCartanMatrix_transpose: the shape of the matrix. Together they certify that it is a symmetric, simply-laced generalized Cartan matrix, which is what an argument embedding this obstruction into an arbitrary diagram has to match against.
• TauCeti.not_isFiniteType_doubleForkCartanMatrix: no affine D̃ₘ matrix for m ≥ 5 is of finite type.

References

This is the affine-D obstruction needed by the “chain/fork length constraints” step in Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4.

@[reducible, inline]

abbrev TauCeti.DoubleForkIndex (n : ℕ) : Type

The indices of the affine D̃ₘ diagram for m = n + 5, parameterized by its n internal vertices between the two forks.

Each outer Fin 2 is the pair of leaves attached to the left, resp. right, fork vertex, so the diagram has four leaves in all. The middle Fin (n + 2) consists of the two fork vertices and the n vertices between them.

Equations

• TauCeti.DoubleForkIndex n = (Fin 2 ⊕ Fin (n + 2) ⊕ Fin 2)

def TauCeti.doubleForkCartanMatrix (n : ℕ) : Matrix (DoubleForkIndex n) (DoubleForkIndex n) ℤ

The Cartan matrix of the affine D̃ₘ diagram for m = n + 5, parameterized by the n internal chain vertices between its two forks.

Equations

• TauCeti.doubleForkCartanMatrix n (Sum.inl i) (Sum.inl j) = if i = j then 2 else 0
• TauCeti.doubleForkCartanMatrix n (Sum.inl val) (Sum.inr (Sum.inl j)) = if ↑j = 0 then -1 else 0
• TauCeti.doubleForkCartanMatrix n (Sum.inl val) (Sum.inr (Sum.inr val_1)) = 0
• TauCeti.doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inl val) = if ↑i = 0 then -1 else 0
• TauCeti.doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl j)) = CartanMatrix.A (n + 2) i j
• TauCeti.doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inr val)) = if ↑i + 1 = n + 2 then -1 else 0
• TauCeti.doubleForkCartanMatrix n (Sum.inr (Sum.inr val)) (Sum.inl val_1) = 0
• TauCeti.doubleForkCartanMatrix n (Sum.inr (Sum.inr val)) (Sum.inr (Sum.inl j)) = if ↑j + 1 = n + 2 then -1 else 0
• TauCeti.doubleForkCartanMatrix n (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inr j)) = if i = j then 2 else 0

def TauCeti.doubleForkMark (n : ℕ) : DoubleForkIndex n → ℚ

The affine marks for D̃ₘ, where m = n + 5: 1 on each of the four leaves and 2 on every vertex of the middle chain.

Equations

• TauCeti.doubleForkMark n (Sum.inl val) = 1
• TauCeti.doubleForkMark n (Sum.inr (Sum.inl val)) = 2
• TauCeti.doubleForkMark n (Sum.inr (Sum.inr val)) = 1

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inl_inl (n : ℕ) (i j : Fin 2) : doubleForkCartanMatrix n (Sum.inl i) (Sum.inl j) = if i = j then 2 else 0

The entries between two left leaves.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inl_inr_inl (n : ℕ) (i : Fin 2) (j : Fin (n + 2)) : doubleForkCartanMatrix n (Sum.inl i) (Sum.inr (Sum.inl j)) = if ↑j = 0 then -1 else 0

The entries from a left leaf to the middle chain.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inl_inr_inr (n : ℕ) (i j : Fin 2) : doubleForkCartanMatrix n (Sum.inl i) (Sum.inr (Sum.inr j)) = 0

The entries from a left leaf to a right leaf.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inr_inl_inl (n : ℕ) (i : Fin (n + 2)) (j : Fin 2) : doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inl j) = if ↑i = 0 then -1 else 0

The entries from the middle chain to a left leaf.

theorem TauCeti.doubleForkCartanMatrix_inr_inl_inr_inl_eq_cartanMatrix_A (n : ℕ) (i j : Fin (n + 2)) : doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl j)) = CartanMatrix.A (n + 2) i j

The middle chain is Mathlib's Cartan matrix of type A. This is not a simp lemma, since CartanMatrix.A has no entry lemma and simp would stall on it.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inr_inl_inr_inl (n : ℕ) (i j : Fin (n + 2)) : doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl j)) = if i = j then 2 else if ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i then -1 else 0

The entries within the middle chain: 2 on the diagonal, and -1 between consecutive vertices of the chain.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inr_inl_inr_inr (n : ℕ) (i : Fin (n + 2)) (j : Fin 2) : doubleForkCartanMatrix n (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inr j)) = if ↑i + 1 = n + 2 then -1 else 0

The entries from the middle chain to a right leaf.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inr_inr_inl (n : ℕ) (i j : Fin 2) : doubleForkCartanMatrix n (Sum.inr (Sum.inr i)) (Sum.inl j) = 0

The entries from a right leaf to a left leaf.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inr_inr_inr_inl (n : ℕ) (i : Fin 2) (j : Fin (n + 2)) : doubleForkCartanMatrix n (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inl j)) = if ↑j + 1 = n + 2 then -1 else 0

The entries from a right leaf to the middle chain.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_inr_inr_inr_inr (n : ℕ) (i j : Fin 2) : doubleForkCartanMatrix n (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inr j)) = if i = j then 2 else 0

The entries between two right leaves.

@[simp]

theorem TauCeti.doubleForkMark_inl (n : ℕ) (i : Fin 2) : doubleForkMark n (Sum.inl i) = 1

Every left leaf has affine mark one.

@[simp]

theorem TauCeti.doubleForkMark_inr_inl (n : ℕ) (i : Fin (n + 2)) : doubleForkMark n (Sum.inr (Sum.inl i)) = 2

Every vertex of the middle chain has affine mark two.

@[simp]

theorem TauCeti.doubleForkMark_inr_inr (n : ℕ) (i : Fin 2) : doubleForkMark n (Sum.inr (Sum.inr i)) = 1

Every right leaf has affine mark one.

theorem TauCeti.doubleForkMark_ne_zero (n : ℕ) : doubleForkMark n ≠ 0

The affine mark vector is nonzero: every leaf has mark 1.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_diag (n : ℕ) (i : DoubleForkIndex n) : doubleForkCartanMatrix n i i = 2

Every diagonal entry of a double-fork Cartan matrix is 2.

theorem TauCeti.isSimplyLaced_doubleForkCartanMatrix (n : ℕ) : (doubleForkCartanMatrix n).IsSimplyLaced

A double-fork Cartan matrix is simply laced: every off-diagonal entry is 0 or -1.

theorem TauCeti.doubleForkCartanMatrix_off_diag_nonpos (n : ℕ) {i j : DoubleForkIndex n} (hij : i ≠ j) : doubleForkCartanMatrix n i j ≤ 0

Every off-diagonal entry of a double-fork Cartan matrix is nonpositive.

theorem TauCeti.doubleForkCartanMatrix_isSymm (n : ℕ) : (doubleForkCartanMatrix n).IsSymm

Every double-fork Cartan matrix is symmetric.

@[simp]

theorem TauCeti.doubleForkCartanMatrix_transpose (n : ℕ) : (doubleForkCartanMatrix n).transpose = doubleForkCartanMatrix n

Transposing a double-fork Cartan matrix leaves it unchanged.

theorem TauCeti.sum_doubleForkCartanMatrix_mul_doubleForkMark_eq_zero (n : ℕ) (i : DoubleForkIndex n) : ∑ j : DoubleForkIndex n, ↑(doubleForkCartanMatrix n i j) * doubleForkMark n j = 0

Every row of a double-fork Cartan matrix annihilates the affine marks. At a leaf the row meets its fork vertex only; at a fork vertex the two leaves cancel the end of the chain the row sum from TauCeti.sum_range_chainEntry_mul leaves over; and in the interior of the chain the row sum vanishes on its own.

This is the shape TauCeti.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos consumes; it is not a simp lemma, since simp dismantles the sum over TauCeti.DoubleForkIndex with the entry lemmas above before this equation could fire.

theorem TauCeti.doubleForkCartanMatrix_mulVec_doubleForkMark_eq_zero (n : ℕ) : ((doubleForkCartanMatrix n).map Int.cast).mulVec (doubleForkMark n) = 0

The standard affine marks form a null vector for the double-fork Cartan matrix.

theorem TauCeti.not_isFiniteType_doubleForkCartanMatrix (n : ℕ) : ¬IsFiniteType (doubleForkCartanMatrix n)

Affine Cartan matrices D̃ₘ for m ≥ 5 are not of finite type. The affine marks are a nonzero null vector, contradicting positive definiteness of any finite-type symmetrization.