Fppf and étale stack descent

The stack layer of this repository was built over the big Zariski site: representableZariskiStack and everything in DerivedAlgGeo.AlgebraicGeometry.Stacks.Algebraic asks only for effective descent along Zariski covers. The standard definition of an algebraic stack asks for descent along fppf covers, or equivalently for the étale formulation, and Zariski descent does not imply either: the finer topologies have covering families the Zariski topology does not.

This file raises the descent level for representable stacks:

• the representableFppfStack and representableEtaleStack abbreviations imported from Stacks/Representable.lean, whose stack condition is Mathlib's fpqc descent theorem for representable presheaves, restricted along Scheme.fppfTopology ≤ Scheme.fpqcTopology and Scheme.etaleTopology ≤ Scheme.fppfTopology;
• Scheme.Cover.toStackCover, turning any Mathlib P-cover into an explicitly indexed covering family, with its fppf, smooth-surjective and étale specializations;
• effective Čech descent along a single faithfully flat morphism locally of finite presentation, which the Zariski layer cannot express because such a morphism need not be a monomorphism;
• the comparisons identifying the existing Zariski layer and the new étale layer as restrictions of the fppf layer.

What this file does not do

It does not define, construct, or assert an algebraic stack, and nothing here should be read as progress toward one beyond the descent level itself. Two of the three prerequisites recorded for stability-families-e15-2 are untouched: the diagonal in Stacks.Algebraic is still represented by schemes rather than by algebraic spaces, and the atlas and diagonal of the full universally-gluable relative-perfect moduli stack are not constructed. No statement about that moduli stack is made here: every stack below is representable.

Covering families for a morphism-property topology

def AlgebraicGeometry.Scheme.Cover.toStackCover {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) : CategoryTheory.StackInGroupoids.Cover S

Every Mathlib P-cover of a scheme is an explicitly indexed covering family for the Grothendieck topology generated by P.

Equations

• 𝒰.toStackCover = { index := 𝒰.I₀, obj := 𝒰.X, hom := 𝒰.f, mem := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.toStackCover_hom {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) (i : 𝒰.I₀) : 𝒰.toStackCover.hom i = 𝒰.f i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.toStackCover_index {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) : 𝒰.toStackCover.index = 𝒰.I₀

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.toStackCover_obj {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) (i : 𝒰.I₀) : 𝒰.toStackCover.obj i = 𝒰.X i

def AlgebraicGeometry.Scheme.fppfCover {X Y : Scheme} (f : X ⟶ Y) [Flat f] [Surjective f] [LocallyOfFinitePresentation f] : CategoryTheory.StackInGroupoids.Cover Y

A faithfully flat morphism locally of finite presentation is a one-element fppf covering family.

Equations

• AlgebraicGeometry.Scheme.fppfCover f = (AlgebraicGeometry.Scheme.Hom.cover f ⋯).toStackCover

def AlgebraicGeometry.Scheme.fppfCoverOfSmoothSurjective {X Y : Scheme} (f : X ⟶ Y) [Smooth f] [Surjective f] : CategoryTheory.StackInGroupoids.Cover Y

A smooth surjection is a one-element fppf covering family, because a smooth morphism is flat and locally of finite presentation.

This is the bridge between the smooth-surjective atlas data already recorded in DerivedAlgGeo.AlgebraicGeometry.Stacks.Algebraic and the fppf descent level. It says that such an atlas is a cover in the right topology; it says nothing about the existence of an atlas for any particular stack.

Equations

• AlgebraicGeometry.Scheme.fppfCoverOfSmoothSurjective f = AlgebraicGeometry.Scheme.fppfCover f

def AlgebraicGeometry.Scheme.etaleCover {X Y : Scheme} (f : X ⟶ Y) [Etale f] [Surjective f] : CategoryTheory.StackInGroupoids.Cover Y

An étale surjection is a one-element étale covering family.

Equations

• AlgebraicGeometry.Scheme.etaleCover f = (AlgebraicGeometry.Scheme.Hom.cover f inst✝¹).toStackCover

@[reducible, inline]

abbrev AlgebraicGeometry.zariskiCoverToFppf {S : Scheme} (U : CategoryTheory.StackInGroupoids.Cover S) : CategoryTheory.StackInGroupoids.Cover S

Every big-Zariski covering family is an fppf covering family, with the same index type and the same arrows.

Equations

• AlgebraicGeometry.zariskiCoverToFppf U = CategoryTheory.StackInGroupoids.Cover.ofLE AlgebraicGeometry.Scheme.zariskiTopology_le_fppfTopology U

@[reducible, inline]

abbrev AlgebraicGeometry.zariskiCoverToEtale {S : Scheme} (U : CategoryTheory.StackInGroupoids.Cover S) : CategoryTheory.StackInGroupoids.Cover S

Every big-Zariski covering family is an étale covering family.

Equations

• AlgebraicGeometry.zariskiCoverToEtale U = CategoryTheory.StackInGroupoids.Cover.ofLE AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology U

Representable stacks at the fppf and étale levels

@[simp]

theorem AlgebraicGeometry.representableFppfStack_presheaf (X : Scheme) : (representableFppfStack X).presheaf = (representableZariskiStack X).presheaf

@[simp]

theorem AlgebraicGeometry.representableEtaleStack_presheaf (X : Scheme) : (representableEtaleStack X).presheaf = (representableZariskiStack X).presheaf

theorem AlgebraicGeometry.representableEtaleStack_eq_ofLE (X : Scheme) : representableEtaleStack X = CategoryTheory.StackInGroupoids.ofLE Scheme.etaleTopology_le_fppfTopology (representableFppfStack X)

The étale level is the restriction of the fppf level along Scheme.etaleTopology ≤ Scheme.fppfTopology.

theorem AlgebraicGeometry.representableZariskiStack_eq_ofLE (X : Scheme) : representableZariskiStack X = CategoryTheory.StackInGroupoids.ofLE Scheme.zariskiTopology_le_fppfTopology (representableFppfStack X)

The existing big-Zariski layer is the restriction of the fppf level.

The implication runs one way only. This recovers the Zariski statement from the fppf one and gives no transport in the other direction, which is why the fppf level had to be proved rather than derived from the Zariski layer.

def AlgebraicGeometry.representableFppfObject {X T : Scheme} (f : T ⟶ X) : ↑((representableFppfStack X).presheaf.obj { as := Opposite.op T })

A morphism T ⟶ X, as an object of the fppf stack represented by X. The fiber categories are literally those of the Zariski layer.

Equations

• AlgebraicGeometry.representableFppfObject f = { as := f }

@[simp]

theorem AlgebraicGeometry.representableFppfObject_eq {X T : Scheme} (f : T ⟶ X) : representableFppfObject f = representableZariskiObject f

Effective fppf and étale descent

noncomputable def AlgebraicGeometry.representableFppfCechDescentEquivalence (X : Scheme) {S : Scheme} (U : CategoryTheory.StackInGroupoids.Cover S) : ↑((representableFppfStack X).presheaf.obj { as := Opposite.op S }) ≌ (representableFppfStack X).CechDescent U

Effective Čech descent for a representable fppf stack along an arbitrary fppf covering family.

Equations

• AlgebraicGeometry.representableFppfCechDescentEquivalence X U = (AlgebraicGeometry.representableFppfStack X).cechDescentEquivalence U

noncomputable def AlgebraicGeometry.representableEtaleCechDescentEquivalence (X : Scheme) {S : Scheme} (U : CategoryTheory.StackInGroupoids.Cover S) : ↑((representableEtaleStack X).presheaf.obj { as := Opposite.op S }) ≌ (representableEtaleStack X).CechDescent U

Effective Čech descent for a representable étale stack along an arbitrary étale covering family.

Equations

• AlgebraicGeometry.representableEtaleCechDescentEquivalence X U = (AlgebraicGeometry.representableEtaleStack X).cechDescentEquivalence U

noncomputable def AlgebraicGeometry.representableFppfDescentAlong (X : Scheme) {Y Z : Scheme} (f : Z ⟶ Y) [Flat f] [Surjective f] [LocallyOfFinitePresentation f] : ↑((representableFppfStack X).presheaf.obj { as := Opposite.op Y }) ≌ (representableFppfStack X).CechDescent (Scheme.fppfCover f)

Effective descent along a single faithfully flat morphism locally of finite presentation.

This is the case the big-Zariski layer cannot express: f is not required to be an open immersion, or even a monomorphism.

Equations

• AlgebraicGeometry.representableFppfDescentAlong X f = (AlgebraicGeometry.representableFppfStack X).cechDescentEquivalence (AlgebraicGeometry.Scheme.fppfCover f)

noncomputable def AlgebraicGeometry.representableFppfDescentAlongSmoothSurjective (X : Scheme) {Y Z : Scheme} (f : Z ⟶ Y) [Smooth f] [Surjective f] : ↑((representableFppfStack X).presheaf.obj { as := Opposite.op Y }) ≌ (representableFppfStack X).CechDescent (Scheme.fppfCoverOfSmoothSurjective f)

Effective descent along a single smooth surjection.

Equations

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

noncomputable def AlgebraicGeometry.representableEtaleDescentAlong (X : Scheme) {Y Z : Scheme} (f : Z ⟶ Y) [Etale f] [Surjective f] : ↑((representableEtaleStack X).presheaf.obj { as := Opposite.op Y }) ≌ (representableEtaleStack X).CechDescent (Scheme.etaleCover f)

Effective descent along a single étale surjection.

Equations

• AlgebraicGeometry.representableEtaleDescentAlong X f = (AlgebraicGeometry.representableEtaleStack X).cechDescentEquivalence (AlgebraicGeometry.Scheme.etaleCover f)

noncomputable def AlgebraicGeometry.representableFppfFullyFaithfulToCechDescent (X : Scheme) {S : Scheme} (U : CategoryTheory.StackInGroupoids.Cover S) : ((representableFppfStack X).toCechDescent U).FullyFaithful

Morphisms of a representable fppf stack satisfy descent: restriction to an fppf cover is fully faithful.

Equations

• AlgebraicGeometry.representableFppfFullyFaithfulToCechDescent X U = (AlgebraicGeometry.representableFppfStack X).fullyFaithfulToCechDescent U

theorem AlgebraicGeometry.representableFppfEssSurjToCechDescent (X : Scheme) {S : Scheme} (U : CategoryTheory.StackInGroupoids.Cover S) : ((representableFppfStack X).toCechDescent U).EssSurj

Objects of a representable fppf stack satisfy effective descent: every fppf Čech descent datum comes from an object over the base.