The affine diagrams B̃ₗ and A⁽²⁾₂ₗ₋₁ are not of finite type

A connected finite-type diagram is a tree of maximal degree three, and the constraints of the Cartan-Killing classification that remain concern where a branch vertex and a multiple edge may sit. The fork bound (TauCeti.eq_zero_or_eq_one_one_or_eq_one_two_le_four_of_isFiniteType_star_three) settles the simply-laced branchings; the rank-two estimates of TauCeti.LinearAlgebra.RootSystem.FiniteType.Basic settle a multiple edge locally; and TauCeti.IsFiniteType.apply_mul_apply_eq_one_of_three_le_card already excludes a multiple edge incident to a branch vertex, since a vertex of degree three meets each of its neighbours along a single edge. What none of them reaches is a double edge at a positive distance from a branch vertex, and the list Aₙ, Bₙ, Cₙ, Dₙ, E₆, E₇, E₈, F₄, G₂ has no such member. This file supplies that step.

The obstruction is the extended Dynkin diagram B̃ₗ, which is exactly the diagram of Bₗ with one further vertex joined to the second vertex of its chain: a fork at one end, a chain, and the double edge of Bₗ at the other end. Adjoining a pendant vertex is the general operation TauCeti.adjoinPendant, and TauCeti.affineBCartanMatrix n is Bₙ₊₃ with a pendant vertex adjoined at the index 1, so that the number of vertices separating the fork from the double edge is arbitrary. An acyclic diagram whose only multiple edge is a double edge, and which has a branch vertex, carries one of these or one of their transposes: keep the path joining the branch vertex to the double edge, two further neighbours of the branch vertex, and nothing else. Carrying that extraction out is left to the step that assembles the classification; what this file provides is the exclusion it needs, in the form TauCeti.IsFiniteType.submatrix consumes.

The certificate is the vector of comarks TauCeti.affineBComark: the value 1 at the two vertices of the fork and at the short vertex beyond the double edge, and 2 at every vertex in between. The Cartan matrix annihilates them, so they are a nonzero subdominant vector and TauCeti.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos excludes the diagram. The transposed family, Cₙ₊₃ with the same pendant vertex adjoined, is the twisted affine diagram A⁽²⁾₂ₗ₋₁, and it is excluded through TauCeti.IsFiniteType.transpose. The rows of the chain are evaluated with TauCeti.sum_range_chainBEntry_mul. Its simply-laced specialization is TauCeti.sum_range_chainEntry_mul, used by TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Basic.

The exclusion is sharp in the only direction available to it: deleting the pendant vertex leaves CartanMatrix.B (n + 3), which TauCeti.isFiniteType_cartanMatrix_B proves to be of finite type, so it is the fork, and not the double edge, that these diagrams die of.

Main definitions

• TauCeti.affineBCartanMatrix: the Cartan matrix of the extended Dynkin diagram B̃ₗ, for ℓ = n + 3.
• TauCeti.affineBComark: its comarks, the test vector the exclusion is proved with.

Main results

• TauCeti.sum_affineBCartanMatrix_mul_affineBComark_eq_zero: the comarks are a null vector of the Cartan matrix.
• TauCeti.not_isFiniteType_affineBCartanMatrix and TauCeti.not_isFiniteType_affineBCartanMatrix_transpose: affineBCartanMatrix n and its transpose, the affine diagrams B̃ₗ and A⁽²⁾₂ₗ₋₁, are not of finite type.

References

This file continues the "chain/fork length constraints" step of the classification of finite-type Cartan matrices, Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The diagram is the affine type B⁽¹⁾ₗ of V. G. Kac, Infinite Dimensional Lie Algebras, 3rd ed., Ch. 4 and Table Aff 1. Kac writes aᵢⱼ = ⟨αⱼ, αᵢ^∨⟩, the transpose of the convention cartanMatrix i j = ⟨αᵢ, αⱼ^∨⟩ used here, so the null vector below is his vector of comarks. See also J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4, where the same configuration is excluded.

The affine diagram B̃ₗ

def TauCeti.affineBCartanMatrix (n : ℕ) : Matrix (Option (Fin (n + 3))) (Option (Fin (n + 3))) ℤ

The Cartan matrix of the extended Dynkin diagram B̃ₗ, for ℓ = n + 3: the chain of Bₗ, whose last edge is double, with one further vertex joined to its second vertex. That second vertex is then joined to three others, and the double edge stands at the far end of the chain, at an arbitrary distance from it - at n = 0 the branch vertex carries the double edge itself.

Equations

• TauCeti.affineBCartanMatrix n = TauCeti.adjoinPendant (CartanMatrix.B (n + 3)) ⟨1, ⋯⟩

theorem TauCeti.affineBCartanMatrix_def (n : ℕ) : affineBCartanMatrix n = adjoinPendant (CartanMatrix.B (n + 3)) ⟨1, ⋯⟩

B̃ₗ as a pendant vertex adjoined to Bₗ. This is not a simp lemma: it would dismantle the left-hand sides of the entry lemmas below, which state the entries of B̃ₗ in its own terms. It is what identifies a diagram extracted from a larger one with this family, together with the entry lemmas.

@[simp]

theorem TauCeti.affineBCartanMatrix_none_some (n : ℕ) (j : Fin (n + 3)) : affineBCartanMatrix n none (some j) = if ↑j = 1 then -1 else 0

The pendant vertex of B̃ₗ is joined to the vertex 1 of the chain alone.

@[simp]

theorem TauCeti.affineBCartanMatrix_some_none (n : ℕ) (j : Fin (n + 3)) : affineBCartanMatrix n (some j) none = if ↑j = 1 then -1 else 0

The pendant vertex of B̃ₗ is joined to the vertex 1 of the chain alone.

@[simp]

theorem TauCeti.affineBCartanMatrix_some_some (n : ℕ) (j k : Fin (n + 3)) : affineBCartanMatrix n (some j) (some k) = CartanMatrix.B (n + 3) j k

Adjoining the pendant vertex changes no entry of the chain of Bₗ.

@[simp]

theorem TauCeti.affineBCartanMatrix_submatrix_some (n : ℕ) : (affineBCartanMatrix n).submatrix some some = CartanMatrix.B (n + 3)

Deleting the pendant vertex of B̃ₗ leaves Bₗ, which is of finite type.

@[simp]

theorem TauCeti.affineBCartanMatrix_transpose (n : ℕ) : (affineBCartanMatrix n).transpose = adjoinPendant (CartanMatrix.C (n + 3)) ⟨1, ⋯⟩

Reversing the double edge of B̃ₗ gives Cₗ with the same pendant vertex, the twisted affine diagram A⁽²⁾₂ₗ₋₁.

@[simp]

theorem TauCeti.affineBCartanMatrix_diag (n : ℕ) (v : Option (Fin (n + 3))) : affineBCartanMatrix n v v = 2

B̃ₗ is a generalized Cartan matrix: its diagonal is 2.

theorem TauCeti.affineBCartanMatrix_apply_le_zero_of_ne (n : ℕ) {v w : Option (Fin (n + 3))} (hvw : v ≠ w) : affineBCartanMatrix n v w ≤ 0

B̃ₗ is a generalized Cartan matrix: its off-diagonal entries are nonpositive.

The rows of B̃ₗ at its comarks

def TauCeti.affineBComark (n : ℕ) : Option (Fin (n + 3)) → ℚ

The comarks of B̃ₗ: the value 1 at the two vertices of the fork and at the short vertex beyond the double edge, and 2 at every vertex of the chain in between.

Along the chain these are the coefficients of the highest root of Bₗ in the basis of simple coroots, θ^∨ = α₁^∨ + 2 α₂^∨ + ⋯ + 2 α_{ℓ-1}^∨ + α_ℓ^∨, and the pendant vertex carries 1: they are the comarks of the affine type B⁽¹⁾ₗ, which is what a null vector of the Cartan matrix is in the convention cartanMatrix i j = ⟨αᵢ, αⱼ^∨⟩ used here.

Equations

• TauCeti.affineBComark n none = 1
• TauCeti.affineBComark n (some j) = if ↑j = 0 ∨ ↑j = n + 2 then 1 else 2

@[simp]

theorem TauCeti.affineBComark_none (n : ℕ) : affineBComark n none = 1

@[simp]

theorem TauCeti.affineBComark_some (n : ℕ) (j : Fin (n + 3)) : affineBComark n (some j) = if ↑j = 0 ∨ ↑j = n + 2 then 1 else 2

theorem TauCeti.affineBComark_pos (n : ℕ) (v : Option (Fin (n + 3))) : 0 < affineBComark n v

The comarks are positive; in particular they are not the zero vector.

theorem TauCeti.sum_affineBCartanMatrix_mul_affineBComark_eq_zero (n : ℕ) (v : Option (Fin (n + 3))) : ∑ w : Option (Fin (n + 3)), ↑(affineBCartanMatrix n v w) * affineBComark n w = 0

The comarks of B̃ₗ are a null vector of its Cartan matrix. This is the certificate the exclusion runs on, stated in the shape TauCeti.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos consumes.

This is not a simp lemma: Fintype.sum_option and the entry lemmas above dismantle the left-hand side before the equation could fire, so the attribute would report only as a simpNF violation.

theorem TauCeti.not_isFiniteType_affineBCartanMatrix (n : ℕ) : ¬IsFiniteType (affineBCartanMatrix n)

The affine diagram B̃ₗ is not of finite type. It is Bₗ with one further vertex adjoined to the second vertex of its chain, so a fork joined by a chain to a double edge; its comarks are a nonzero subdominant vector, indeed a null vector, so TauCeti.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos excludes it.

For n ≥ 1 no earlier elimination reaches it: it is a genuine generalized Cartan matrix, its branch vertex has degree three, its one double edge is the only multiple edge and has Cartan product 2, which the rank-two estimates allow, and the fork bound applies to simply-laced stars only. At n = 0 the branch vertex carries the double edge itself, and TauCeti.IsFiniteType.apply_mul_apply_eq_one_of_three_le_card - a branch vertex is simply laced - already excludes that member.

theorem TauCeti.not_isFiniteType_affineBCartanMatrix_transpose (n : ℕ) : ¬IsFiniteType (affineBCartanMatrix n).transpose

The same diagram with its double edge reversed is not of finite type either. Transposing B̃ₗ reverses every edge, so it fixes the pendant edge and the chain and turns the double edge of Bₗ into that of Cₗ, giving the twisted affine diagram A⁽²⁾₂ₗ₋₁. The two orientations are the two ways a double edge can face a branch vertex, so together with TauCeti.not_isFiniteType_affineBCartanMatrix this rules out both.