Documentation

TauCeti.Algebra.Lie.Orthogonal.TypeB.GeneratorRelations

Cartan action on the split type-B root generators #

This file records the coordinates of the Bourbaki simple coroots in the split diagonal Cartan and uses them to compute their action on both signs of every simple root. If dᵢ is the coordinate vector of the ith simple coroot, the formulas are

[hᵢ, eⱼ] = dᵢ(j) eⱼ                         (j the short node),
[hᵢ, eⱼ] = (dᵢ(j) - dᵢ(j+1)) eⱼ            (j a long node),

with the negatives of these scalars on the negative-root generators. The results below identify these scalars uniformly with entries of Mathlib's type-B Cartan matrix; the transpose appears because the coroot index comes first in the Lie bracket. The mixed and higher Serre relations are subsequent steps.

Main results #

References #

These relations supply matrix-model input both to the Chevalley--Demazure construction and to a Chevalley-style basis of the split type-B Lie algebra.

source
def TauCeti.typeBSimpleCorootCoordinate {K : Type u} [CommRing K] {n : ℕ} (i : Fin (n + 1)) :
Fin (n + 1) → K

The coordinate vector of a Bourbaki simple coroot of Bₙ₊₁ in the split diagonal Cartan. The first n nodes are εᵢ - εᵢ₊₁, while the final short node has coroot 2εₙ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootCoordinate_last {K : Type u} [CommRing K] {n : ℕ} :
    typeBSimpleCorootCoordinate (Fin.last n) = 2 • Pi.single (Fin.last n) 1
    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootCoordinate_castSucc {K : Type u} [CommRing K] {n : ℕ} (i : Fin n) :
    typeBSimpleCorootCoordinate i.castSucc = Pi.single i.castSucc 1 - Pi.single i.succ 1
    source
    theorem TauCeti.typeBSimpleCorootGenerator_eq_diagonal {K : Type u} [CommRing K] {n : ℕ} (i : Fin (n + 1)) :
    typeBSimpleCorootGenerator i = ↑(typeBDiagonalEquiv (typeBSimpleCorootCoordinate i))

    A simple coroot generator is the split diagonal element with the corresponding coordinate vector.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_eq_zero {K : Type u} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) :
    ⁅typeBSimpleCorootGenerator i, typeBSimpleCorootGenerator j⁆ = 0

    The simple coroot generators in the standard split type-B model commute.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_root_last {K : Type u} [CommRing K] {n : ℕ} (i : Fin (n + 1)) :
    ⁅typeBSimpleCorootGenerator i, typeBShortRootGenerator (Fin.last n)⁆ = typeBSimpleCorootCoordinate i (Fin.last n) • typeBShortRootGenerator (Fin.last n)

    The action of a simple coroot on the positive generator at the final short node.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_root_castSucc {K : Type u} [CommRing K] {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    ⁅typeBSimpleCorootGenerator i, typeBDifferenceRootGenerator j.castSucc j.succ ⋯⁆ = (typeBSimpleCorootCoordinate i j.castSucc - typeBSimpleCorootCoordinate i j.succ) • typeBDifferenceRootGenerator j.castSucc j.succ ⋯

    The action of a simple coroot on a positive generator at a long node.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_negativeRoot_last {K : Type u} [CommRing K] {n : ℕ} (i : Fin (n + 1)) :
    ⁅typeBSimpleCorootGenerator i, typeBShortNegativeRootGenerator (Fin.last n)⁆ = -typeBSimpleCorootCoordinate i (Fin.last n) • typeBShortNegativeRootGenerator (Fin.last n)

    The action of a simple coroot on the negative generator at the final short node.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_negativeRoot_castSucc {K : Type u} [CommRing K] {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    ⁅typeBSimpleCorootGenerator i, typeBDifferenceRootGenerator j.succ j.castSucc ⋯⁆ = (typeBSimpleCorootCoordinate i j.succ - typeBSimpleCorootCoordinate i j.castSucc) • typeBDifferenceRootGenerator j.succ j.castSucc ⋯

    The action of a simple coroot on a negative generator at a long node.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_root {K : Type u} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) :
    ⁅typeBSimpleCorootGenerator i, typeBSimpleRootGenerator j⁆ = CartanMatrix.B (n + 1) j i • typeBSimpleRootGenerator j

    The Cartan action on positive simple-root generators, in Serre's integral convention.

    source
    @[simp]
    theorem TauCeti.typeBSimpleCorootGenerator_lie_negativeRoot {K : Type u} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) :
    ⁅typeBSimpleCorootGenerator i, typeBSimpleNegativeRootGenerator j⁆ = -(CartanMatrix.B (n + 1) j i • typeBSimpleNegativeRootGenerator j)

    The Cartan action on negative simple-root generators, in Serre's integral convention.

    source
    theorem TauCeti.typeBSimpleCorootGenerator_ne_zero {K : Type u} [CommRing K] {n : ℕ} [NeZero 2] (i : Fin (n + 1)) :
    typeBSimpleCorootGenerator i ≠ 0

    Each simple coroot generator is nonzero away from characteristic two.

    source
    theorem TauCeti.isSl2Triple_typeBSimpleRootGenerator {K : Type u} [CommRing K] {n : ℕ} [NeZero 2] (i : Fin (n + 1)) :
    IsSl2Triple (typeBSimpleCorootGenerator i) (typeBSimpleRootGenerator i) (typeBSimpleNegativeRootGenerator i)

    The positive and negative simple-root generators at each type-B node, together with the simple coroot generator, form an sl₂ triple.