Row primitivity of the type-D Cartan matrix

In rank at least three, every row of the type-D Cartan matrix CartanMatrix.D n contains an entry -1. A node of the chain, other than the last two, uses its successor along the chain; the two fork nodes use the branch node n - 3 they are both attached to. Rank two is the exception: D₂ is A₁ × A₁, whose rows (2, 0) and (0, 2) generate only 2ℤ.

This file names such a neighbour TauCeti.typeDCartanNeighbor and packages the resulting Bezout certificate TauCeti.typeDCartanBezout, 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 D 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, and it is shared by every carrier built on the type-D Serre presentation.

Main declarations

• TauCeti.typeDCartanNeighbor: a node adjacent to a given node with Cartan entry -1.
• TauCeti.cartanMatrixD_typeDCartanNeighbor: in rank at least three, that Cartan entry is -1.
• TauCeti.typeDCartanBezout and TauCeti.sum_cartanMatrixD_mul_typeDCartanBezout: the explicit Bezout certificate for each row of the type-D Cartan matrix.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
• TauCeti.LinearAlgebra.Matrix.Cartan.TypeB, whose type-B certificate this file mirrors.

def TauCeti.typeDCartanNeighbor (n : ℕ) (i : Fin n) : Fin n

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

Equations

• TauCeti.typeDCartanNeighbor n i = ⟨if ↑i + 2 < n then ↑i + 1 else n - 3, ⋯⟩

@[simp]

theorem TauCeti.val_typeDCartanNeighbor {n : ℕ} (i : Fin n) : ↑(typeDCartanNeighbor n i) = if ↑i + 2 < n then ↑i + 1 else n - 3

@[simp]

theorem TauCeti.cartanMatrixD_typeDCartanNeighbor {n : ℕ} (hn : 3 ≤ n) (i : Fin n) : CartanMatrix.D n i (typeDCartanNeighbor n i) = -1

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

def TauCeti.typeDCartanBezout (n : ℕ) (i j : Fin n) : ℤ

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

Equations

• TauCeti.typeDCartanBezout n i j = if j = TauCeti.typeDCartanNeighbor n i then -1 else 0

@[simp]

theorem TauCeti.typeDCartanBezout_apply {n : ℕ} (i j : Fin n) : typeDCartanBezout n i j = if j = typeDCartanNeighbor n i then -1 else 0

theorem TauCeti.sum_cartanMatrixD_mul_typeDCartanBezout {n : ℕ} (hn : 3 ≤ n) (i : Fin n) : ∑ j : Fin n, CartanMatrix.D n i j * typeDCartanBezout n i j = 1

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