Row primitivity of the type-B Cartan matrix

In rank at least three, every row of the type-B Cartan matrix CartanMatrix.B r contains an entry -1. The final row uses the -1 entry on its side of the double bond. The second-to-last row has entry -2 across that bond, but in rank at least three it also has a -1 entry towards the preceding node. The other rows use a neighbouring entry along the single-bond chain. Rank two is the exception: the long-root row of B₂ is (2, -2), whose entries generate only 2ℤ.

This file names such a neighbour TauCeti.typeBCartanNeighbor and packages the resulting Bezout certificate TauCeti.typeBCartanBezout, the integer coefficients -1 at that neighbour and 0 elsewhere, whose pairing with the Cartan row is 1. It says that every simple root of type B in rank at least three is a primitive character of a split torus whose weights are the Cartan rows. This is the arithmetic hypothesis in TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup_le_kostantElementarySubgroup.

Main declarations

• TauCeti.typeBCartanNeighbor: a node adjacent to a given node with Cartan entry -1.
• TauCeti.cartanMatrixB_typeBCartanNeighbor: in rank at least three, that Cartan entry is -1.
• TauCeti.typeBCartanBezout and TauCeti.sum_cartanMatrixB_mul_typeBCartanBezout: the explicit Bezout certificate for each row of the type-B Cartan matrix.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II.
• TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.Generation.

def TauCeti.typeBCartanNeighbor (r : ℕ) (i : Fin r) : Fin r

A column index chosen as the successor of i, except at the last two indices, where it is the predecessor. In rank at least three this is an adjacent node of the type-B Dynkin diagram, with Cartan entry -1 in row i.

Equations

• TauCeti.typeBCartanNeighbor r i = ⟨if ↑i + 2 < r then ↑i + 1 else ↑i - 1, ⋯⟩

@[simp]

theorem TauCeti.val_typeBCartanNeighbor {r : ℕ} (i : Fin r) : ↑(typeBCartanNeighbor r i) = if ↑i + 2 < r then ↑i + 1 else ↑i - 1

theorem TauCeti.cartanMatrixB_typeBCartanNeighbor {r : ℕ} (hr : 3 ≤ r) (i : Fin r) : CartanMatrix.B r i (typeBCartanNeighbor r i) = -1

In rank at least three, the type-B Cartan matrix has entry -1 at each node and its chosen neighbour.

def TauCeti.typeBCartanBezout (r : ℕ) (i j : Fin r) : ℤ

Integer coefficients supported at the chosen column: -1 at typeBCartanNeighbor r i and 0 elsewhere. They certify row primitivity in rank at least three.

Equations

• TauCeti.typeBCartanBezout r i j = if j = TauCeti.typeBCartanNeighbor r i then -1 else 0

@[simp]

theorem TauCeti.typeBCartanBezout_apply {r : ℕ} (i j : Fin r) : typeBCartanBezout r i j = if j = typeBCartanNeighbor r i then -1 else 0

theorem TauCeti.sum_cartanMatrixB_mul_typeBCartanBezout {r : ℕ} (hr : 3 ≤ r) (i : Fin r) : ∑ j : Fin r, CartanMatrix.B r i j * typeBCartanBezout r i j = 1

In rank at least three, every row of the type-B Cartan matrix is a primitive integer vector, with the explicit certificate typeBCartanBezout.