Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Dynamic.Weight.Levi.Decomposition

The limit morphism from a weight parabolic to its Levi subgroup #

Let w : Fin N → ℤ and let P(w) and L(w) be the represented weight parabolic and Levi subgroups of GL_N. The dynamic limit

g ↦ lim_{t → 0} diag(t ^ w) g diag(t ^ (-w))

is natural in the commutative value algebra. Yoneda therefore represents it by a morphism of coordinate Hopf algebras O(L(w)) → O(P(w)), and hence by a group-scheme morphism P(w) → L(w). Its effect on points is exactly the dynamic limit, not merely an abstract existence statement.

This is the retraction needed to extract the Levi coordinate in the represented semidirect-product decomposition of P(w).

Main declarations #

References #

This advances the dynamic route to parabolic subgroups and Levi decomposition in Layer 7, "Structure theory", of the ReductiveGroups roadmap. The remaining step is to combine this represented retraction with the represented unipotent and Levi inclusions to identify P(w) with their semidirect product.

source
noncomputable def TauCeti.GeneralLinear.Dynamic.weightParabolicLimitPointsMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

The natural transformation on represented points obtained by transporting the dynamic limit from the weight parabolic to the weight Levi.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.GeneralLinear.Dynamic.weightParabolicLimitPointsMap_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
    weightParabolicLimitPointsMap R w = CategoryTheory.CategoryStruct.comp (weightParabolicPointsIso R w).hom (CategoryTheory.CategoryStruct.comp (Cocharacter.limitToLeviNatTrans (weightCocharacter w)) (weightLeviPointsIso R w).inv)

    The represented limit map is the dynamic limit transported through the representing isomorphisms for the weight parabolic and weight Levi.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.Dynamic.weightParabolicLimitPointsMap_app_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom ((weightParabolicLimitPointsMap R w).app A)) g = (CategoryTheory.ConcreteCategory.hom ((weightLeviPointsIso R w).inv.app A)) ((Cocharacter.limitToLevi (↑A) (weightCocharacter w)) ((CategoryTheory.ConcreteCategory.hom ((weightParabolicPointsIso R w).hom.app A)) g))

    At every value algebra, the represented limit map is the dynamic limit transported through the representing isomorphisms for the weight parabolic and weight Levi.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.Dynamic.mapPointsFunctor_weightLeviToParabolicCoordinateMap_comp_weightParabolicLimitPointsMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
    CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mapPointsFunctor (weightLeviToParabolicCoordinateMap R w)) (weightParabolicLimitPointsMap R w) = CategoryTheory.CategoryStruct.id HopfAlgebra.pointsFunctor

    The canonical represented Levi inclusion is a section of the represented dynamic limit.

    source
    noncomputable def TauCeti.GeneralLinear.Dynamic.weightParabolicLimitCoordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
    weightLeviCoordinateHopfAlgebra R w ⟶ weightParabolicCoordinateHopfAlgebra R w

    The coordinate morphism representing the limit P(w) → L(w). Its direction is O(L(w)) → O(P(w)), opposite to the group-scheme morphism.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.weightParabolicLimitCoordinateMap_comp_weightLeviToParabolicCoordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
      CategoryTheory.CategoryStruct.comp (weightParabolicLimitCoordinateMap R w) (weightLeviToParabolicCoordinateMap R w) = CategoryTheory.CategoryStruct.id (weightLeviCoordinateHopfAlgebra R w)

      The limit coordinate morphism is a section of the coordinate morphism representing the Levi inclusion. This is the coordinate-ring form of the retraction P(w) → L(w).

      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.mapPointsFunctor_weightParabolicLimitCoordinateMap_app (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
      (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightParabolicLimitCoordinateMap R w)).app A)) g = (CategoryTheory.ConcreteCategory.hom ((weightLeviPointsIso R w).inv.app A)) ((Cocharacter.limitToLevi (↑A) (weightCocharacter w)) ((CategoryTheory.ConcreteCategory.hom ((weightParabolicPointsIso R w).hom.app A)) g))

      On every commutative value algebra, the morphism induced by the limit coordinate map is the dynamic limit transported to the represented weight-Levi points.

      source
      noncomputable def TauCeti.GeneralLinear.Dynamic.weightParabolicLimit (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
      weightParabolicGroupScheme R w ⟶ weightLeviGroupScheme R w

      The group-scheme morphism P(w) → L(w) represented by the dynamic limit.

      Equations
      Instances For
        source
        theorem TauCeti.GeneralLinear.Dynamic.weightParabolicLimit_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        weightParabolicLimit R w = (AlgebraicGeometry.hopfSpec ↧R).map (weightParabolicLimitCoordinateMap R w).op

        The weight-parabolic limit is relative spectrum applied contravariantly to its coordinate Hopf-algebra morphism.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.Dynamic.schemePointsAlgΓMulEquiv_weightParabolicLimit (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)) (g : T ⟶ (weightParabolicGroupScheme R w).X) :
        WithConv.toConv (CommAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.algΓ ↧R).map g) ((AlgebraicGeometry.algΓ ↧R).map (weightParabolicLimit R w).hom.hom)) ((AlgebraicGeometry.algΓAlgSpecAdjunction ↧R).counit.app (Opposite.op ↧↑(weightLeviCoordinateHopfAlgebra R w)))).unop) = (CategoryTheory.ConcreteCategory.hom ((weightLeviPointsIso R w).inv.app (Opposite.unop ((AlgebraicGeometry.algΓ ↧R).obj T)))) ((Cocharacter.limitToLevi (↑(Opposite.unop ((AlgebraicGeometry.algΓ ↧R).obj T))) (weightCocharacter w)) ((CategoryTheory.ConcreteCategory.hom ((weightParabolicPointsIso R w).hom.app (Opposite.unop ((AlgebraicGeometry.algΓ ↧R).obj T)))) ((CommHopfAlgCat.schemePointsAlgΓMulEquiv (↑(weightParabolicCoordinateHopfAlgebra R w)) T) g)))

        On points valued in an arbitrary scheme over Spec R, the group-scheme limit is the dynamic limit over the relative global sections of that scheme.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.Dynamic.weightLeviToParabolic_comp_weightParabolicLimit (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        CategoryTheory.CategoryStruct.comp (weightLeviToParabolic R w) (weightParabolicLimit R w) = CategoryTheory.CategoryStruct.id (weightLeviGroupScheme R w)

        The represented dynamic limit retracts the existing closed immersion of the weight Levi into the weight parabolic.