Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.RootSubgroup.Differential

Differentials of symplectic root subgroups #

The differential of each represented root map ๐”พโ‚ โ†’ Spโ‚‚โ‚˜ sends an additive tangent parameter to the corresponding single matrix unit (long roots) or signed pair of matrix units (short roots). This identifies its image with the line spanned by its normalized unit tangent vector, and proves injectivity over arbitrary commutative coefficient algebras, including nonreduced rings and characteristic two. These are the Lie vectors used to normalize the type-C root subgroups in a pinning.

The coordinate calculation uses Symplectic.rootSubgroupCoordinateMap_apply_X, the quotient tangent map, and Symplectic.tangentLieEquivSp. Its organization follows SpecialLinear.Root.Differential, with all five symplectic root families treated uniformly through GLSymplecticFin.RootSubgroupIndex.tangentMatrix.

References #

source
@[simp]
theorem TauCeti.Symplectic.tangentMatrix_derivationComp_rootSubgroup {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} (root : GLSymplecticFin.RootSubgroupIndex m) (d : Derivation R (โ†‘(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (โ†‘(AdditiveGroup.coordinateHopfAlgebra R)) B)) :
โ†‘((tangentMatrix m) ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap root))) d)) = root.tangentMatrix (AdditiveGroup.gaTangentLinearEquiv d)

The represented root-subgroup differential has the standard normalized symplectic matrix: a single entry for a long root and a signed pair for a short root.

source
theorem TauCeti.Symplectic.derivationComp_rootSubgroup_injective {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} (root : GLSymplecticFin.RootSubgroupIndex m) :
Function.Injective โ‡‘(derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap root)))

Every root-subgroup differential is injective over every commutative coefficient algebra.

source
noncomputable def TauCeti.Symplectic.rootVector {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} (root : GLSymplecticFin.RootSubgroupIndex m) :
Derivation R (โ†‘(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (โ†‘(coordinateHopfAlgebra R m)) B)

The normalized root vector is the image of the additive unit tangent vector under the represented root-subgroup differential.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Symplectic.tangentMatrix_rootVector {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} (root : GLSymplecticFin.RootSubgroupIndex m) :
    โ†‘((tangentMatrix m) (rootVector root)) = root.tangentMatrix 1

    The matrix of the normalized root vector has parameter one.

    source
    theorem TauCeti.Symplectic.derivationComp_rootSubgroup_eq_smul_rootVector {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} (root : GLSymplecticFin.RootSubgroupIndex m) (d : Derivation R (โ†‘(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (โ†‘(AdditiveGroup.coordinateHopfAlgebra R)) B)) :
    (derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap root))) d = AdditiveGroup.gaTangentLinearEquiv d โ€ข rootVector root

    The differential sends a tangent parameter to that scalar times the normalized root vector.

    source
    theorem TauCeti.Symplectic.range_derivationCompLieHom_rootSubgroup_eq_span {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} (root : GLSymplecticFin.RootSubgroupIndex m) :
    (derivationCompLieHom (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap root))).range.toSubmodule = B โˆ™ rootVector root

    The image of a root-subgroup differential is exactly its normalized root line.

    source
    theorem TauCeti.Symplectic.rootVector_ne_zero {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {m : โ„•} [Nontrivial B] (root : GLSymplecticFin.RootSubgroupIndex m) :
    rootVector root โ‰  0

    The normalized root vector is nonzero whenever the coefficient algebra is nontrivial.