Documentation

TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.ClosedRootSubgroup

Closed root subgroups of the type-D full-spin carrier #

For every Bourbaki node of type D_n, the raising and lowering root-subgroup maps into TauCeti.TypeDSpinCarrier.groupScheme n hn are closed copies of the additive group scheme.

The proof reads a unit coefficient directly from the exterior model of the full spin representation. Along the chain, creation at one coordinate after annihilation at the next sends one singleton exterior-basis vector to another. At the fork, the positive operator creates the last two coordinates from the vacuum, while the negative operator annihilates them back to the vacuum. The generic Kostant root-subgroup criterion then makes the coordinate map surjective.

Main declarations #

References #

This supplies the closed-root-subgroup component of the type-D pinning required by Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its downstream consumer is milestone L0 of the CFSGStatement roadmap.

source
theorem TauCeti.TypeDSpinCarrier.rootSubgroupCoordinateMap_surjective (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) k))

The coordinate morphism of every numbered type-D full-spin root subgroup is surjective.

source
instance TauCeti.TypeDSpinCarrier.isClosedImmersion_rootSubgroup (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup n hn k).hom.hom)

Every numbered root-subgroup map into the type-D full-spin carrier is a closed immersion.

source
theorem TauCeti.TypeDSpinCarrier.mono_rootSubgroup (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
CategoryTheory.Mono (rootSubgroup n hn k)

Every numbered root-subgroup map into the type-D full-spin carrier is a monomorphism.

source
noncomputable def TauCeti.TypeDSpinCarrier.rootSubgroupClosedSubgroup (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
ClosedSubgroupScheme (groupScheme n hn)

A numbered type-D full-spin root subgroup, bundled as a closed subgroup scheme.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.TypeDSpinCarrier.coe_rootSubgroupClosedSubgroup (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
    ↑(rootSubgroupClosedSubgroup n hn k) = CategoryTheory.Subobject.mk (rootSubgroup n hn k)

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

    source
    noncomputable def TauCeti.TypeDSpinCarrier.rootSubgroupClosedSubgroupIso (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
    CategoryTheory.Subobject.underlying.obj ↑(rootSubgroupClosedSubgroup n hn k) ≅ AdditiveGroup.groupScheme ℤ

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

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

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