Documentation

TauCeti.Algebra.AlgebraicGroup.Center.Quotient

The fppf quotient by the center #

Let H be the coordinate Hopf algebra of an affine group over a field. The center is a normal closed subgroup, so the general fppf quotient construction gives the center quotient G / Z(G) as a group object in fppf sheaves. This file names that quotient and its canonical projection.

The projection is an epimorphism and is locally surjective for the fppf topology. Its kernel-pair square is the torsor square for the action of the center on G. The sheaf quotient is the correct first construction of G / Z(G): no representability claim is made here. For a reductive group, representability and the proof that the represented quotient is the adjoint form remain separate.

Before sheafification, the construction is the ordinary quotient G(A) / Z(G)(A) on every commutative value algebra A. Its projection has kernel exactly the universally central points.

Main declarations #

References #

source
theorem TauCeti.CommHopfAlgCat.isNormal_centerDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) :
(centerDefiningIdeal H).IsNormal

The defining Hopf ideal of the center is normal.

source
theorem TauCeti.CommHopfAlgCat.centerPointsSubgroupNormal {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) :
(centerPointsSubgroup H A).Normal

Locally expose normality of the represented center on points.

source
@[reducible, inline]
noncomputable abbrev TauCeti.CommHopfAlgCat.centerPointwiseQuotient {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) :
GrpCat

The pointwise center quotient G(A) / Z(G)(A).

The fppf center quotient is obtained by assembling these groups into a presheaf and sheafifying.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def TauCeti.CommHopfAlgCat.centerPointwiseQuotientGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) :
    Group ↑(centerPointwiseQuotient H A)

    Locally expose the group structure carried by the bundled pointwise center quotient.

    Equations
    Instances For
      source
      noncomputable def TauCeti.CommHopfAlgCat.centerPointwiseQuotientMk {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) :
      HopfAlgebra.points A ⟶ centerPointwiseQuotient H A

      The quotient homomorphism from G(A) to G(A) / Z(G)(A).

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.centerPointwiseQuotientMk_apply {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientMk H A)) g = (QuotientGroup.mk' (centerPointsSubgroup H A)) g

        The pointwise center-quotient projection sends a point to its ordinary quotient class.

        source
        theorem TauCeti.CommHopfAlgCat.centerPointwiseQuotientMk_ker {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) :
        (GrpCat.Hom.hom (centerPointwiseQuotientMk H A)).ker = HopfAlgebra.center k ↑H ↑A

        The kernel of G(A) ⟶ G(A) / Z(G)(A) is exactly the A-points of the represented center.

        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.centerPointwiseQuotientMk_eq_one_iff_isCentralPoint {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientMk H A)) g = 1 ↔ HopfAlgebra.IsCentralPoint g

        A point maps to the identity in G(A) / Z(G)(A) exactly when it is universally central.

        source
        theorem TauCeti.CommHopfAlgCat.centerPointwiseQuotientMk_surjective {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) :
        Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientMk H A))

        The projection from points to their center quotient is surjective.

        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.mapPointwiseQuotient_centerPointwiseQuotientMk {k : Type u} [Field k] (H : CommHopfAlgCat k) {A B : CommAlgCat k} (φ : A ⟶ B) (g : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom (mapPointwiseQuotient H (centerDefiningIdeal H) ⋯ φ)) ((CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientMk H A)) g) = (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientMk H B)) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints φ)) g)

        Extension of scalars sends a center-quotient class to the class of the extended point.

        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.CommHopfAlgCat.centerQuotientFppfSheaf {k : Type u} [Field k] (H : CommHopfAlgCat k) :
        CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1)))

        The fppf sheaf quotient G / Z(G) of an affine group by its center.

        This is the sheafification of the pointwise quotient presheaf. It does not assert that the quotient is represented by a scheme.

        Equations
        Instances For
          source
          noncomputable def TauCeti.CommHopfAlgCat.centerQuotientFppfProjection {k : Type u} [Field k] (H : CommHopfAlgCat k) :
          pointsFppfGroupObject H ⟶ centerQuotientFppfSheaf H

          The canonical morphism from an affine group's fppf sheaf of points to its center quotient.

          Equations
          Instances For
            source
            noncomputable def TauCeti.CommHopfAlgCat.centerQuotientFppfHomEquiv {k : Type u} [Field k] (H : CommHopfAlgCat k) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1)))) :
            (centerQuotientFppfSheaf H ⟶ F) ≃ (pointwiseQuotientPresheafGrp H (centerDefiningIdeal H) ⋯ ⟶ fppfGroupObjectToPresheaf F)

            Maps from the center quotient to an fppf sheaf group are equivalent to maps from the pointwise center quotient into its underlying presheaf.

            Equations
            Instances For
              source
              noncomputable def TauCeti.CommHopfAlgCat.centerQuotientFppfLift {k : Type u} [Field k] (H : CommHopfAlgCat k) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1)))) (f : pointwiseQuotientPresheafGrp H (centerDefiningIdeal H) ⋯ ⟶ fppfGroupObjectToPresheaf F) :
              centerQuotientFppfSheaf H ⟶ F

              A map from the pointwise center quotient into the underlying presheaf of an fppf sheaf group extends uniquely to the fppf center quotient.

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.CommHopfAlgCat.centerQuotientFppfHomEquiv_centerQuotientFppfLift {k : Type u} [Field k] (H : CommHopfAlgCat k) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1)))) (f : pointwiseQuotientPresheafGrp H (centerDefiningIdeal H) ⋯ ⟶ fppfGroupObjectToPresheaf F) :
                (centerQuotientFppfHomEquiv H F) (centerQuotientFppfLift H F f) = f

                The universal-property equivalence sends the center-quotient lift back to the supplied map.

                source
                theorem TauCeti.CommHopfAlgCat.centerQuotientFppfLift_unique {k : Type u} [Field k] (H : CommHopfAlgCat k) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1)))) (f : pointwiseQuotientPresheafGrp H (centerDefiningIdeal H) ⋯ ⟶ fppfGroupObjectToPresheaf F) (g : centerQuotientFppfSheaf H ⟶ F) (hg : (centerQuotientFppfHomEquiv H F) g = f) :
                g = centerQuotientFppfLift H F f

                A morphism from the center quotient is determined by its image under the universal-property equivalence.

                source
                instance TauCeti.CommHopfAlgCat.instEpiCenterQuotientFppfProjection {k : Type u} [Field k] (H : CommHopfAlgCat k) :
                CategoryTheory.Epi (centerQuotientFppfProjection H)

                The projection to the fppf center quotient is an epimorphism.

                source
                theorem TauCeti.CommHopfAlgCat.isLocallySurjective_centerQuotientFppfProjection {k : Type u} [Field k] (H : CommHopfAlgCat k) :
                CategoryTheory.Sheaf.IsLocallySurjective (centerQuotientFppfProjection H).hom.hom

                Every section of the fppf center quotient lifts to an ambient-group section after an fppf cover.

                source
                @[reducible, inline]
                noncomputable abbrev TauCeti.CommHopfAlgCat.centerQuotientFppfTorsorAction {k : Type u} [Field k] (H : CommHopfAlgCat k) :
                CategoryTheory.MonoidalCategoryStruct.tensorObj (pointsFppfGroupObject H).X (pointsFppfGroupObject (quotient H (centerDefiningIdeal H))).X ⟶ (pointsFppfGroupObject H).X

                The right action of the center on the ambient fppf sheaf of points.

                Equations
                Instances For
                  source
                  theorem TauCeti.CommHopfAlgCat.isPullback_centerQuotientFppfTorsor {k : Type u} [Field k] (H : CommHopfAlgCat k) :
                  CategoryTheory.IsPullback (CategoryTheory.SemiCartesianMonoidalCategory.fst (pointsFppfGroupObject H).X (pointsFppfGroupObject (quotient H (centerDefiningIdeal H))).X) (centerQuotientFppfTorsorAction H) (centerQuotientFppfProjection H).hom.hom (centerQuotientFppfProjection H).hom.hom

                  The kernel pair of G ⟶ G / Z(G) is G × Z(G) via (g, z) ↦ (g, gz). Together with local surjectivity, this exhibits the projection as an fppf torsor under the center.