Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Kernel.Presheaf

Pointwise quotients by scheme-theoretic kernels #

For a morphism f : H ⟶ K of commutative Hopf algebras, the induced affine-group morphism goes in the opposite direction, from the group represented by K to the group represented by H. Its scheme-theoretic kernel is cut out by kernelHopfIdeal f.

This file proves the pointwise first-isomorphism comparison. The kernel Hopf ideal is normal, so the pointwise quotient by it is defined. Precomposition with f then descends to a natural map

K(A) / ker(f)(A) ⟶ H(A),

and this map is injective for every value algebra A. It is an isomorphism whenever the map on A-points is surjective. Thus the pointwise quotient identifies naturally with the image of the represented morphism; the remaining representability step in the fppf first isomorphism theorem is to prove local, rather than pointwise, surjectivity under the usual flatness hypotheses.

Main declarations #

References #

source
noncomputable def TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) :
pointwiseQuotientGroup K (kernelHopfIdeal f) ⋯ A ⟶ HopfAlgebra.points A

At a value algebra A, precomposition with f descends from source points to the quotient by the scheme-theoretic kernel.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom (kernelPointwiseQuotientMap f A)) ((CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk K (kernelHopfIdeal f) ⋯ A)) g) = (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A)) g

    The kernel-quotient comparison sends the class of a source point to its image under f.

    source
    theorem TauCeti.CommHopfAlgCat.mapPointwiseQuotient_comp_kernelPointwiseQuotientMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {A B : CommAlgCat R} (χ : A ⟶ B) :
    CategoryTheory.CategoryStruct.comp (mapPointwiseQuotient K (kernelHopfIdeal f) ⋯ χ) (kernelPointwiseQuotientMap f B) = CategoryTheory.CategoryStruct.comp (kernelPointwiseQuotientMap f A) (HopfAlgebra.mapPoints χ)

    The kernel-quotient comparisons are natural in the value algebra.

    source
    noncomputable def TauCeti.CommHopfAlgCat.kernelPointwiseQuotientNatTrans {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    pointwiseQuotientFunctor K (kernelHopfIdeal f) ⋯ ⟶ HopfAlgebra.pointsFunctor

    The kernel-quotient comparisons, bundled as a natural transformation from the pointwise quotient presheaf to the target functor of points.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientNatTrans_app {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) :
      (kernelPointwiseQuotientNatTrans f).app A = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (kernelPointwiseQuotientMap f A) (CategoryTheory.eqToHom ⋯))

      A component of the natural kernel-quotient comparison is the corresponding pointwise map.

      source
      theorem TauCeti.CommHopfAlgCat.pointwiseQuotientProjection_comp_kernelPointwiseQuotientNatTrans {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      CategoryTheory.CategoryStruct.comp (pointwiseQuotientProjection K (kernelHopfIdeal f) ⋯) (kernelPointwiseQuotientNatTrans f) = mapPointsFunctor f

      The natural kernel-quotient comparison factors the map on points through the pointwise quotient projection.

      source
      theorem TauCeti.CommHopfAlgCat.pointwiseQuotientProjection_comp_kernelPointwiseQuotientNatTrans_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {Z : CategoryTheory.Functor (CommAlgCat R) GrpCat} (h : HopfAlgebra.pointsFunctor ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (pointwiseQuotientProjection K (kernelHopfIdeal f) ⋯) (CategoryTheory.CategoryStruct.comp (kernelPointwiseQuotientNatTrans f) h) = CategoryTheory.CategoryStruct.comp (mapPointsFunctor f) h

      The natural kernel-quotient comparison factors the map on points through the pointwise quotient projection.

      source
      theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap_injective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) :
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (kernelPointwiseQuotientMap f A))

      The comparison from the quotient by the scheme-theoretic kernel to target points is injective over every value algebra.

      source
      instance TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap_mono {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) :
      CategoryTheory.Mono (kernelPointwiseQuotientMap f A)

      Every component of the natural kernel-quotient comparison is a monomorphism of groups.

      source
      instance TauCeti.CommHopfAlgCat.kernelPointwiseQuotientNatTrans_mono {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      CategoryTheory.Mono (kernelPointwiseQuotientNatTrans f)

      The natural kernel-quotient comparison is a monomorphism.

      source
      theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap_surjective_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) :
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (kernelPointwiseQuotientMap f A)) ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A))

      The kernel-quotient comparison is surjective exactly when the original map on points is surjective.

      source
      theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap_isIso_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) :
      CategoryTheory.IsIso (kernelPointwiseQuotientMap f A) ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A))

      The kernel-quotient comparison is an isomorphism exactly when f is surjective on points over the chosen value algebra.

      source
      theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientMap_isIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) (hsurj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A))) :
      CategoryTheory.IsIso (kernelPointwiseQuotientMap f A)

      A surjective map on A-points induces an isomorphism from the pointwise kernel quotient to the target group of A-points.

      source
      noncomputable def TauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) (hsurj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A))) :
      pointwiseQuotientGroup K (kernelHopfIdeal f) ⋯ A ≅ HopfAlgebra.points A

      Pointwise first isomorphism theorem for affine groups. If the morphism represented by f is surjective on A-points, the target group of points is isomorphic to the pointwise quotient of source points by the scheme-theoretic kernel.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.kernelPointwiseQuotientIso_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (A : CommAlgCat R) (hsurj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A))) :
        (kernelPointwiseQuotientIso f A hsurj).hom = kernelPointwiseQuotientMap f A

        The forward map of the pointwise first-isomorphism equivalence is the canonical kernel-quotient comparison.