Documentation

TauCeti.Algebra.AlgebraicGroup.Fppf.Quotient.Torsor

The fppf quotient projection as a torsor #

Let H be a commutative Hopf algebra over a commutative ring R, and let I be a normal Hopf ideal. The quotient Hopf algebra H / I represents the closed normal subgroup V(I) of the affine group represented by H. This file proves the kernel-pair formulation of the statement that

G ⟶ G / V(I)

is a V(I)-torsor: the square

G × V(I)  --(g,n) ↦ g-->    G
    |                         |
 (g,n) ↦ gn               | quotient
    |                         |
    v                         v
    G          --quotient-->  G / V(I)

is a pullback. It is first proved for the pointwise quotient presheaf. Applying fppf sheafification and its canonical finite-product comparison gives the corresponding pullback square on the product of the fppf sheaves.

No representability of G / V(I) is asserted.

Main declarations #

References #

This is the torsor and kernel-pair step of Layer 3, "Normality and quotients", of the ReductiveGroups roadmap.

source
noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientTorsorAction {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
CategoryTheory.MonoidalCategoryStruct.tensorObj (pointsPresheafGrp H).X (pointsPresheafGrp (quotient H I)).X ⟶ (pointsPresheafGrp H).X

The action map in the pointwise torsor square, (g, n) ↦ gn.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.pointwiseQuotientTorsorAction_app {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (A : (CommAlgCat R)ᵒᵖᵒᵖ) :
    (pointwiseQuotientTorsorAction H I).app A = TypeCat.ofHom fun (p : ULift.{u + 1, u} ↑(HopfAlgebra.points (Opposite.unop (Opposite.unop A))) × ULift.{u + 1, u} ↑(HopfAlgebra.points (Opposite.unop (Opposite.unop A)))) => { down := p.1.down * (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I (Opposite.unop (Opposite.unop A)))) p.2.down }
    source
    theorem TauCeti.CommHopfAlgCat.isPullback_pointwiseQuotientTorsor {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) :
    CategoryTheory.IsPullback (CategoryTheory.SemiCartesianMonoidalCategory.fst (pointsPresheafGrp H).X (pointsPresheafGrp (quotient H I)).X) (pointwiseQuotientTorsorAction H I) (pointwiseQuotientPresheafGrpProjection H I hI).hom.hom (pointwiseQuotientPresheafGrpProjection H I hI).hom.hom

    The pointwise quotient projection has the expected torsor kernel pair: two ambient points have the same quotient class exactly when they differ by a unique point of the closed subgroup represented by H / I.

    source
    noncomputable def TauCeti.CommHopfAlgCat.fppfQuotientTorsorProductIso {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (pointsFppfGroupObject H).X (pointsFppfGroupObject (quotient H I)).X ≅ (CategoryTheory.presheafToSheaf (CommAlgCat.fppfTopology R) (Type (u + 1))).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (pointsPresheafGrp H).X (pointsPresheafGrp (quotient H I)).X)

    The canonical comparison from the product of the two fppf sheaves to the sheafification of their pointwise product. This is the inverse of the product comparison supplied by the left exactness of fppf sheafification, after identifying the two sheafified factors with the carriers of their fppf group objects.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def TauCeti.CommHopfAlgCat.quotientSubgroupPointsFppfGrpInclusion {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
      pointsFppfGroupObject (quotient H I) ⟶ pointsFppfGroupObject H

      The inclusion of the closed subgroup represented by H / I into the ambient fppf group.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def TauCeti.CommHopfAlgCat.fppfQuotientTorsorAction {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
        CategoryTheory.MonoidalCategoryStruct.tensorObj (pointsFppfGroupObject H).X (pointsFppfGroupObject (quotient H I)).X ⟶ (pointsFppfGroupObject H).X

        The action map in the sheafified torsor square, defined on the product of the ambient and subgroup fppf sheaves.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem TauCeti.CommHopfAlgCat.fppfQuotientTorsorAction_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) :
          fppfQuotientTorsorAction H I = CategoryTheory.SemiCartesianMonoidalCategory.fst (pointsFppfGroupObject H).toMon.X (pointsFppfGroupObject (quotient H I)).toMon.X * CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (pointsFppfGroupObject H).toMon.X (pointsFppfGroupObject (quotient H I)).toMon.X) (quotientSubgroupPointsFppfGrpInclusion H I).hom.hom

          The quotient torsor action multiplies an ambient point by a subgroup point.

          source
          @[simp]
          theorem CommHopfAlgCat.sheafify_pointwiseQuotientTorsorFst {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) :
          CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientTorsorProductIso H I).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1))).map (CategoryTheory.SemiCartesianMonoidalCategory.fst (TauCeti.CommHopfAlgCat.pointsPresheafGrp H).X (TauCeti.CommHopfAlgCat.pointsPresheafGrp (TauCeti.CommHopfAlgCat.quotient H I)).X)) (CategoryTheory.eqToHom ⋯)) = CategoryTheory.SemiCartesianMonoidalCategory.fst (TauCeti.CommHopfAlgCat.pointsFppfGroupObject H).X (TauCeti.CommHopfAlgCat.pointsFppfGroupObject (TauCeti.CommHopfAlgCat.quotient H I)).X

          Sheafification identifies the first projection of the pointwise torsor product with the first projection of the product of fppf point sheaves.

          source
          @[simp]
          theorem CommHopfAlgCat.sheafify_pointwiseQuotientTorsorFst_assoc {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) {Z : CategoryTheory.Sheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1))} (h : (TauCeti.CommHopfAlgCat.pointsFppfGroupObject H).X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientTorsorProductIso H I).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1))).map (CategoryTheory.SemiCartesianMonoidalCategory.fst (TauCeti.CommHopfAlgCat.pointsPresheafGrp H).X (TauCeti.CommHopfAlgCat.pointsPresheafGrp (TauCeti.CommHopfAlgCat.quotient H I)).X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (TauCeti.CommHopfAlgCat.pointsFppfGroupObject H).X (TauCeti.CommHopfAlgCat.pointsFppfGroupObject (TauCeti.CommHopfAlgCat.quotient H I)).X) h

          Sheafification identifies the first projection of the pointwise torsor product with the first projection of the product of fppf point sheaves.

          source
          @[simp]
          theorem CommHopfAlgCat.sheafify_pointwiseQuotientTorsorAction {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) :
          CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientTorsorProductIso H I).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1))).map (TauCeti.CommHopfAlgCat.pointwiseQuotientTorsorAction H I)) (CategoryTheory.eqToHom ⋯)) = TauCeti.CommHopfAlgCat.fppfQuotientTorsorAction H I

          Sheafification identifies multiplication by subgroup points with the action on the product of fppf point sheaves.

          source
          @[simp]
          theorem CommHopfAlgCat.sheafify_pointwiseQuotientTorsorAction_assoc {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) {Z : CategoryTheory.Sheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1))} (h : (TauCeti.CommHopfAlgCat.pointsFppfGroupObject H).X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientTorsorProductIso H I).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (u + 1))).map (TauCeti.CommHopfAlgCat.pointwiseQuotientTorsorAction H I)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) = CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.fppfQuotientTorsorAction H I) h

          Sheafification identifies multiplication by subgroup points with the action on the product of fppf point sheaves.

          source
          theorem TauCeti.CommHopfAlgCat.isPullback_fppfQuotientTorsor {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) :
          CategoryTheory.IsPullback (CategoryTheory.SemiCartesianMonoidalCategory.fst (pointsFppfGroupObject H).X (pointsFppfGroupObject (quotient H I)).X) (fppfQuotientTorsorAction H I) (fppfQuotientProjection H I hI).hom.hom (fppfQuotientProjection H I hI).hom.hom

          The kernel pair of the fppf quotient projection G ⟶ G / V(I) is G × V(I) via (g,n) ↦ (g,gn). Together with isLocallySurjective_fppfQuotientProjection, this gives the two torsor conditions.