The fppf first isomorphism theorem for affine groups

Let f : H ⟶ K be a morphism of commutative Hopf algebras over R. Contravariantly it represents a homomorphism Spec K ⟶ Spec H of affine groups whose scheme-theoretic kernel is cut out by kernelHopfIdeal f. The pointwise comparison K(A) / ker(f)(A) ⟶ H(A) is injective for every value algebra A, but it is surjective only when f is surjective on A-points.

This file sheafifies that comparison. If the coordinate map f is faithfully flat and of finite presentation, every A-point y of Spec H lifts to a point of Spec K after the fppf cover A ⟶ A ⊗[H] K, so the comparison is locally surjective as well as injective. Its sheafification is therefore an isomorphism

Spec K / ker(f) ≅ Spec H

of group objects in fppf sheaves. In other words, a faithfully flat finitely presented homomorphism of affine groups exhibits its target as the fppf quotient of its source by its kernel, and that quotient is representable. Under this isomorphism the quotient projection is the morphism of fppf points induced by f.

Main declarations

• TauCeti.CommHopfAlgCat.kernelFppfQuotientHom: the comparison from the fppf quotient by the kernel to the fppf points of the target.
• TauCeti.CommHopfAlgCat.fppfQuotientProjection_comp_kernelFppfQuotientHom: the comparison carries the quotient projection to the morphism pointsFppfGroupObjectMap f induced by f.
• TauCeti.CommHopfAlgCat.isIso_kernelFppfQuotientHom: the comparison is an isomorphism when f is faithfully flat and of finite presentation.
• TauCeti.CommHopfAlgCat.kernelFppfQuotientIso: the fppf first isomorphism theorem.

References

• J. S. Milne, Algebraic Groups (2017), Section 5.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Sections 14--15.

noncomputable def TauCeti.CommHopfAlgCat.kernelFppfQuotientHom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : fppfQuotientSheaf K (kernelHopfIdeal f) ⋯ ⟶ pointsFppfGroupObject H

The comparison from the fppf quotient of Spec K by the kernel of f to the fppf points of Spec H, obtained by sheafifying the pointwise kernel-quotient comparison.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.fppfQuotientProjection_comp_kernelFppfQuotientHom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp (fppfQuotientProjection K (kernelHopfIdeal f) ⋯) (kernelFppfQuotientHom f) = pointsFppfGroupObjectMap f

The fppf kernel-quotient comparison carries the quotient projection Spec K ⟶ Spec K / ker f to the morphism of fppf points induced by f.

@[simp]

theorem TauCeti.CommHopfAlgCat.fppfQuotientProjection_comp_kernelFppfQuotientHom_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {Z : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))} (h : pointsFppfGroupObject H ⟶ Z) : CategoryTheory.CategoryStruct.comp (fppfQuotientProjection K (kernelHopfIdeal f) ⋯) (CategoryTheory.CategoryStruct.comp (kernelFppfQuotientHom f) h) = CategoryTheory.CategoryStruct.comp (pointsFppfGroupObjectMap f) h

The fppf kernel-quotient comparison carries the quotient projection Spec K ⟶ Spec K / ker f to the morphism of fppf points induced by f.

theorem TauCeti.CommHopfAlgCat.isIso_kernelFppfQuotientHom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hflat : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) (hfp : (↑(CommHopfAlgCat.Hom.hom f)).FinitePresentation) : CategoryTheory.IsIso (kernelFppfQuotientHom f)

If f is faithfully flat and of finite presentation, the comparison from the fppf quotient of Spec K by the kernel of f to the fppf points of Spec H is an isomorphism of group objects in fppf sheaves.

noncomputable def TauCeti.CommHopfAlgCat.kernelFppfQuotientIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hflat : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) (hfp : (↑(CommHopfAlgCat.Hom.hom f)).FinitePresentation) : fppfQuotientSheaf K (kernelHopfIdeal f) ⋯ ≅ pointsFppfGroupObject H

The fppf first isomorphism theorem for affine groups. If f : H ⟶ K is faithfully flat and of finite presentation, then the fppf quotient of Spec K by the kernel of the represented homomorphism Spec K ⟶ Spec H is represented by Spec H.

Equations

• TauCeti.CommHopfAlgCat.kernelFppfQuotientIso f hflat hfp = CategoryTheory.asIso (TauCeti.CommHopfAlgCat.kernelFppfQuotientHom f)

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelFppfQuotientIso_hom {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hflat : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) (hfp : (↑(CommHopfAlgCat.Hom.hom f)).FinitePresentation) : (kernelFppfQuotientIso f hflat hfp).hom = kernelFppfQuotientHom f

The forward map of the fppf first isomorphism is the kernel-quotient comparison.