Affine-group points on the affine fppf site

For a commutative ring R, the category (CommAlgCat R)ᵒᵖ is the category of affine schemes over Spec R. The imported generic affine-site module equips it with the fppf topology induced by Mathlib's fppf topology on schemes over Spec R. Thus a presheaf on this site has the expected variance

CommAlgCat R ⥤ Type.

For a commutative Hopf algebra H, the imported Yoneda module registers the underlying type-valued presheaf of convolution points A ↦ WithConv (H →ₐ[R] A) as representable. Its representability and subcanonicity imply that affine-group points form an fppf sheaf.

This is the affine-site foundation for fppf sheafification of pointwise quotients. It does not assert that such a quotient sheaf is representable; representability requires separate hypotheses.

Main declarations

• TauCeti.HopfAlgebra.pointsPresheaf_isSheaf: affine-group points satisfy fppf descent.
• TauCeti.HopfAlgebra.pointsFppfSheaf: affine-group points bundled as an fppf sheaf.

References

• J. S. Milne, Algebraic Groups (2017), Sections 2 and 5.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Sections 1 and 14.

This advances the cross-cutting sheaves-and-descent prerequisite and Layer 3, "Normality and quotients", of the ReductiveGroups roadmap. The next step is to sheafify the existing pointwise quotient presheaf and prove its quotient universal property in the fppf topos.

theorem TauCeti.HopfAlgebra.pointsPresheaf_isSheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Presheaf.IsSheaf (CommAlgCat.fppfTopology R) (pointsPresheaf H)

Affine-group points form an fppf sheaf. The type-valued convolution-points presheaf is representable on the opposite site because the original covariant points functor is corepresentable.

theorem TauCeti.HopfAlgebra.pointsGroupPresheaf_isSheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Presheaf.IsSheaf (CommAlgCat.fppfTopology R) (pointsGroupPresheaf H)

The group-valued convolution-points presheaf is an fppf sheaf. This is the group-valued form of pointsPresheaf_isSheaf; the forgetful functor from groups preserves limits and reflects isomorphisms.

noncomputable def TauCeti.HopfAlgebra.pointsFppfSheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) GrpCat

The convolution-points functor, bundled as a group-valued sheaf on the affine fppf site.

Equations

• TauCeti.HopfAlgebra.pointsFppfSheaf H = { obj := TauCeti.HopfAlgebra.pointsGroupPresheaf H, property := ⋯ }

@[simp]

theorem TauCeti.HopfAlgebra.pointsFppfSheaf_obj {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsFppfSheaf H).obj = pointsGroupPresheaf H

The presheaf underlying pointsFppfSheaf is the convolution-points presheaf.