The affine fppf site

For a commutative ring R, this file equips (CommAlgCat R)ᵒᵖ with the topology induced by Mathlib's fppf topology on schemes over Spec R. This is the category of affine schemes over Spec R, presented contravariantly through their coordinate algebras.

The induced affine topology is subcanonical by full faithfulness of the relative spectrum functor.

Main declarations

• TauCeti.CommAlgCat.fppfTopology: the fppf topology on opposite commutative R-algebras.
• TauCeti.CommAlgCat.fppfTopology_subcanonical: affine representable functors are fppf sheaves.
• TauCeti.CommAlgCat.isCoverDense_algSpec: relative spectra of R-algebras are cover-dense among schemes over Spec R, so a sieve is an affine fppf cover exactly when its image is.
• TauCeti.CommAlgCat.generate_singleton_op_mem_fppfTopology: a faithfully flat, finitely presented algebra map is an affine fppf cover.

This advances the cross-cutting sheaves-and-descent prerequisite in the ReductiveGroups roadmap.

noncomputable def TauCeti.CommAlgCat.fppfTopology (R : Type u) [CommRing R] : CategoryTheory.GrothendieckTopology (CommAlgCat R)ᵒᵖ

The fppf topology on affine schemes over Spec R, expressed on the equivalent category (CommAlgCat R)ᵒᵖ.

It is the topology induced along the relative spectrum functor from the fppf topology on schemes over Spec R.

Equations

• TauCeti.CommAlgCat.fppfTopology R = (AlgebraicGeometry.algSpec ↧R).inducedTopology (AlgebraicGeometry.Scheme.fppfTopology.over (AlgebraicGeometry.Spec ↧R))

theorem TauCeti.CommAlgCat.fppfTopology_def (R : Type u) [CommRing R] : fppfTopology R = (AlgebraicGeometry.algSpec ↧R).inducedTopology (AlgebraicGeometry.Scheme.fppfTopology.over (AlgebraicGeometry.Spec ↧R))

The affine fppf topology is induced from the fppf topology on schemes over Spec R.

instance TauCeti.CommAlgCat.fppfTopology_subcanonical (R : Type u) [CommRing R] : (fppfTopology R).Subcanonical

The affine fppf topology is subcanonical. Every presheaf represented by an affine scheme over Spec R is an fppf sheaf.

instance TauCeti.CommAlgCat.isCoverDense_algSpec (R : Type u) [CommRing R] : (AlgebraicGeometry.algSpec ↧R).IsCoverDense (AlgebraicGeometry.Scheme.fppfTopology.over (AlgebraicGeometry.Spec ↧R))

Every scheme over Spec R is covered by affine opens, and an affine open, with the R-algebra structure induced by its structure morphism, is the relative spectrum of an R-algebra. So relative spectra are cover-dense for the fppf topology over Spec R.

theorem TauCeti.CommAlgCat.generate_singleton_op_mem_fppfTopology {R : Type u} [CommRing R] {A B : CommAlgCat R} (φ : A ⟶ B) (hflat : (CommAlgCat.Hom.hom φ).FaithfullyFlat) (hfp : (CommAlgCat.Hom.hom φ).FinitePresentation) : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton φ.op) ∈ (fppfTopology R) (Opposite.op A)

A faithfully flat, finitely presented algebra map is an fppf cover. If φ : A ⟶ B is faithfully flat and of finite presentation, then the sieve generated by the corresponding morphism Spec B ⟶ Spec A covers Spec A in the affine fppf topology.