Documentation

TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.ClosedRootSubgroup

Closed root subgroups of the type-B spin carrier #

For every Bourbaki node of type Bₙ₊₁, the raising and lowering root-subgroup maps into TauCeti.TypeBSpinCarrier.groupScheme n are closed copies of the additive group scheme.

The spin representation makes the required unit matrix coefficient explicit. At a nonterminal node, the raising and lowering operators move an exterior singleton between two adjacent coordinates. At the terminal short node, they create or annihilate the final coordinate, with the distinguished remainder vector acting by exterior parity. The generic Kostant root-subgroup criterion then makes the coordinate-ring homomorphism surjective.

Main declarations #

References #

Unit-coefficient exterior-basis steps #

Closed root-subgroup morphisms #

source
theorem TauCeti.TypeBSpinCarrier.rootSubgroupCoordinateMap_surjective (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) k))

The coordinate-ring homomorphism of every numbered type-Bₙ₊₁ spin root subgroup is surjective.

source
instance TauCeti.TypeBSpinCarrier.isClosedImmersion_rootSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup n k).hom.hom)

Every numbered root-subgroup map into the type-Bₙ₊₁ spin carrier is a closed immersion.

source
theorem TauCeti.TypeBSpinCarrier.mono_rootSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
CategoryTheory.Mono (rootSubgroup n k)

Every numbered root-subgroup map into the type-Bₙ₊₁ spin carrier is a monomorphism.

source
noncomputable def TauCeti.TypeBSpinCarrier.rootSubgroupClosedSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
ClosedSubgroupScheme (groupScheme n)

A numbered type-Bₙ₊₁ spin root subgroup, bundled as a closed subgroup scheme.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.TypeBSpinCarrier.coe_rootSubgroupClosedSubgroup (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
    ↑(rootSubgroupClosedSubgroup n k) = CategoryTheory.Subobject.mk (rootSubgroup n k)

    The bundled closed root subgroup is represented by the numbered root-subgroup morphism.

    source
    noncomputable def TauCeti.TypeBSpinCarrier.rootSubgroupClosedSubgroupIso (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
    CategoryTheory.Subobject.underlying.obj ↑(rootSubgroupClosedSubgroup n k) ≅ AdditiveGroup.groupScheme ℤ

    The bundled numbered root subgroup is canonically isomorphic to the additive group scheme.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.TypeBSpinCarrier.rootSubgroupClosedSubgroupIso_inv_comp_arrow (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) :
      CategoryTheory.CategoryStruct.comp (rootSubgroupClosedSubgroupIso n k).inv (↑(rootSubgroupClosedSubgroup n k)).arrow = rootSubgroup n k

      The canonical parametrization followed by inclusion is the numbered root-subgroup map.