Documentation

TauCeti.Algebra.AlgebraicGroup.Dynamic.Levi.Quotient

The dynamic Levi as an fppf quotient #

For a cocharacter λ of an affine group scheme, the limit morphism on the dynamic parabolic factors through the dynamic Levi. Its section is the Levi inclusion and its scheme-theoretic kernel is the dynamic unipotent subgroup. Consequently the fppf quotient P(λ)/U(λ) is represented by Z(λ), compatibly with the limit projection.

These statements hold over an arbitrary commutative base ring, without smoothness, reductivity or finite-type hypotheses, and retain the full subgroup scheme structures. They supply the quotient interpretation of the dynamic Levi decomposition.

The construction uses the represented limit in Dynamic.Limit and the fppf first isomorphism theorem CommHopfAlgCat.isIso_kernelFppfQuotientHom_of_exists_lift. The Levi section provides global lifts over every value algebra.

References #

source
noncomputable def BialgHom.parabolicLimitToLeviCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
(↧H).quotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l) ⟶ (↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)

The coordinate morphism of the dynamic limit with codomain the Levi subgroup: contravariantly, O(Z(λ)) → O(P(λ)).

Instances For
    source
    @[simp]
    theorem BialgHom.mkQuotient_comp_parabolicLimitToLeviCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    CategoryTheory.CategoryStruct.comp ((↧H).mkQuotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l)) l.parabolicLimitToLeviCoordinateMap = l.parabolicLimitCoordinateMap

    The Levi-valued limit followed by the ambient Levi inclusion is the represented limit.

    source
    @[simp]
    theorem BialgHom.mkQuotient_comp_parabolicLimitToLeviCoordinateMap_assoc {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {Z : CommHopfAlgCat R} (h : (↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((↧H).mkQuotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l)) (CategoryTheory.CategoryStruct.comp l.parabolicLimitToLeviCoordinateMap h) = CategoryTheory.CategoryStruct.comp l.parabolicLimitCoordinateMap h

    The Levi-valued limit followed by the ambient Levi inclusion is the represented limit.

    source
    @[simp]
    theorem BialgHom.parabolicLimitToLeviCoordinateMap_mk {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (h : H) :
    (CommHopfAlgCat.Hom.hom l.parabolicLimitToLeviCoordinateMap) ((CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l))) h) = (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l))) (((TauCeti.Cocharacter.conjugationAlgHom l) h).coeff 0)

    On a quotient class, the Levi-valued limit sends a function to the constant Laurent coefficient of its conjugation family, restricted to the parabolic.

    source
    @[simp]
    theorem BialgHom.parabolicLimitToLeviCoordinateMap_comp_quotientMapOfLe {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    CategoryTheory.CategoryStruct.comp l.parabolicLimitToLeviCoordinateMap ((↧H).quotientMapOfLe ⋯) = CategoryTheory.CategoryStruct.id ((↧H).quotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l))

    Inclusion of the dynamic Levi is a section of the Levi-valued limit.

    source
    @[simp]
    theorem BialgHom.parabolicLimitToLeviCoordinateMap_comp_quotientMapOfLe_assoc {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {Z : CommHopfAlgCat R} (h : (↧H).quotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp l.parabolicLimitToLeviCoordinateMap (CategoryTheory.CategoryStruct.comp ((↧H).quotientMapOfLe ⋯) h) = h

    Inclusion of the dynamic Levi is a section of the Levi-valued limit.

    source
    theorem BialgHom.kernelHopfIdeal_parabolicLimitToLeviCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    TauCeti.CommHopfAlgCat.kernelHopfIdeal l.parabolicLimitToLeviCoordinateMap = l.unipotentDefiningHopfIdeal.map (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)))

    The kernel of the Levi-valued dynamic limit is the dynamic unipotent subgroup, with its defining ideal transported into the parabolic coordinate algebra.

    source
    theorem BialgHom.quotientPointsHom_parabolicLimitToLeviCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) (g : ↑(TauCeti.HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom (TauCeti.CommHopfAlgCat.quotientPointsHom (↧H) (TauCeti.Cocharacter.leviDefiningHopfIdeal l) A)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.Hom.mapPointsFunctor l.parabolicLimitToLeviCoordinateMap).app A)) g) = (TauCeti.Cocharacter.limit (↑A) l) ((CategoryTheory.ConcreteCategory.hom ((TauCeti.Cocharacter.parabolicPointsIso l).hom.app A)) g)

    On every value algebra, the ambient point of the Levi-valued limit is the dynamic limit of the represented parabolic point.

    source
    theorem BialgHom.isNormal_unipotentDefiningHopfIdeal_map_parabolic {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    (l.unipotentDefiningHopfIdeal.map (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)))).IsNormal

    The dynamic unipotent subgroup is normal in the represented dynamic parabolic.

    source
    instance BialgHom.isIso_kernelFppfQuotientHom_parabolicLimitToLeviCoordinateMap {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    CategoryTheory.IsIso (TauCeti.CommHopfAlgCat.kernelFppfQuotientHom l.parabolicLimitToLeviCoordinateMap)

    The kernel-quotient comparison for the Levi-valued limit is an isomorphism of fppf sheaf groups. The Levi section lifts every point over its original value algebra.

    source
    noncomputable def BialgHom.parabolicLeviFppfQuotientIso {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    TauCeti.CommHopfAlgCat.fppfQuotientSheaf ((↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)) (l.unipotentDefiningHopfIdeal.map (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)))) ⋯ ≅ TauCeti.CommHopfAlgCat.pointsFppfGroupObject ((↧H).quotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l))

    The fppf quotient P(λ)/U(λ) is the dynamic Levi Z(λ). The subgroup in the quotient is given by its actual defining ideal inside the parabolic coordinate ring.

    Instances For
      source
      @[simp]
      theorem BialgHom.fppfQuotientProjection_comp_parabolicLeviFppfQuotientIso_hom {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
      CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientProjection ((↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)) (l.unipotentDefiningHopfIdeal.map (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)))) ⋯) l.parabolicLeviFppfQuotientIso.hom = TauCeti.CommHopfAlgCat.pointsFppfGroupObjectMap l.parabolicLimitToLeviCoordinateMap

      The quotient identification carries the projection onto P(λ)/U(λ) to the dynamic limit with values in the Levi.

      source
      @[simp]
      theorem BialgHom.fppfQuotientProjection_comp_parabolicLeviFppfQuotientIso_hom_assoc {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {Z : CategoryTheory.Grp (CategoryTheory.Sheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1)))} (h : TauCeti.CommHopfAlgCat.pointsFppfGroupObject ((↧H).quotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l)) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientProjection ((↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)) (l.unipotentDefiningHopfIdeal.map (CommHopfAlgCat.Hom.hom ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l)))) ⋯) (CategoryTheory.CategoryStruct.comp l.parabolicLeviFppfQuotientIso.hom h) = CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.pointsFppfGroupObjectMap l.parabolicLimitToLeviCoordinateMap) h

      The quotient identification carries the projection onto P(λ)/U(λ) to the dynamic limit with values in the Levi.