Documentation

TauCeti.Algebra.Lie.Orthogonal.TypeD.Root.PositiveSpan

Generation of the positive type-D root vectors #

The positive roots of type Dₙ are εᵢ - εⱼ and εᵢ + εⱼ for i < j. This file shows directly on the split orthogonal matrix carrier that their standard root vectors belong to the Lie subalgebra generated by the numbered positive simple-root vectors.

For the difference roots, successive brackets concatenate intervals along the chain. For the sum roots, the fork generator first produces every sum root involving the last coordinate; a generated difference root then moves the second coordinate from the last index to any j with i < j < n - 1. The imported matrix bracket identities record the signs used in these recurrences.

Main declarations #

References #

The positive simple-root span #

source
noncomputable def TauCeti.TypeDStd.positiveSimpleRootMatrixLieSpan {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) :
LieSubalgebra K ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)

The Lie subalgebra of the split type-D matrix Lie algebra generated by its numbered positive simple-root vectors.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.TypeDStd.rootGenerator_inl_mem_positiveSimpleRootMatrixLieSpan {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) :
    rootGenerator n hn (Sum.inl i) ∈ positiveSimpleRootMatrixLieSpan n hn

    Every numbered positive simple-root vector belongs to their generated Lie subalgebra.

    source
    @[simp]
    theorem TauCeti.TypeDStd.positiveSimpleRootMatrixLieSpan_le_iff {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (S : LieSubalgebra K ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)) :
    positiveSimpleRootMatrixLieSpan n hn ≤ S ↔ ∀ (i : Fin n), rootGenerator n hn (Sum.inl i) ∈ S

    The positive simple-root matrix span lies in a Lie subalgebra exactly when every numbered positive simple-root vector lies in it.

    Generation of all positive roots #

    source
    theorem TauCeti.TypeDStd.differenceRootGenerator_mem_positiveSimpleRootMatrixLieSpan {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i j : Fin n) (hij : i < j) :
    differenceRootGenerator i j ∈ positiveSimpleRootMatrixLieSpan n hn

    Every positive difference-root vector εᵢ - εⱼ, with i < j, belongs to the Lie subalgebra generated by the positive simple-root vectors.

    source
    theorem TauCeti.TypeDStd.sumRootGenerator_mem_positiveSimpleRootMatrixLieSpan {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i j : Fin n) (hij : i < j) :
    sumRootGenerator i j ∈ positiveSimpleRootMatrixLieSpan n hn

    Every positive sum-root vector εᵢ + εⱼ, with i < j, belongs to the Lie subalgebra generated by the positive simple-root vectors.