Stack presentations at the fppf level

Stacks/Algebraic.lean builds presentation data -- a representable diagonal, an atlas scheme, a smooth-surjective atlas, and local finite presentation over a base -- and says of it, in its own words, that it is not an algebraic stack: the standard notion asks for fppf descent, and that file only ever asks for Zariski descent.

Stacks/Representable.lean supplies representableFppfStack, whose stack condition is Mathlib's fpqc descent theorem for representable presheaves restricted along Scheme.fppfTopology ≤ Scheme.fpqcTopology.

This file puts the two together. The presentations below are the same data as the big-Zariski ones, over stacks whose descent is fppf.

What is and is not claimed

The diagonal here is represented by schemes, not by algebraic spaces. That is stronger than the usual condition, not weaker, so a presentation in this file is more than the definition asks for on that axis -- but it also means these are not literally the standard AlgebraicStack of the literature, and they are not named as though they were. No Artin representability theorem is postulated, here or anywhere below it: every atlas, diagonal and finiteness datum is an actual scheme morphism statement carried in the structure.

Why the fppf layer costs almost nothing here

representableFppfStack X and representableZariskiStack X have the same presheaf -- both are discretePseudofunctor (yoneda.obj X), and representableFppfStack_presheaf proves it by rfl. They differ only in which descent theorem they carry, which is a Prop field.

A StackMorphism, its FiberRepresentation, and the representability vocabulary generalized over an arbitrary topology in Stacks/Algebraic.lean all speak about presheaves and about representing scheme morphisms. None mentions a covering family. So the fppf morphism is the Zariski morphism, and the constructions below are definitional transports rather than new proofs. That is the content of representableFppfStackMap_eq_zariski: it is rfl, and it is stated precisely so the reader does not have to take the claim on trust.

This is not a claim that fppf descent is free. It is the observation that the work of proving it was already done in Stacks/Descent.lean, and that nothing in the presentation vocabulary needed redoing once it stopped naming a topology it never used.

The fppf representable stack map

def AlgebraicGeometry.representableFppfStackMap {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.StackMorphism (representableFppfStack X) (representableFppfStack Y)

A scheme morphism induces the corresponding morphism of representable big-fppf stacks.

This is the big-Zariski morphism unchanged: the two stacks have the same presheaf, and a StackMorphism is data about presheaves.

Equations

• AlgebraicGeometry.representableFppfStackMap f = CategoryTheory.StackInGroupoids.representableMap AlgebraicGeometry.Scheme.fppfTopology f

theorem AlgebraicGeometry.representableFppfStackMap_eq_zariski {X Y : Scheme} (f : X ⟶ Y) : representableFppfStackMap f = representableZariskiStackMap f

The fppf and Zariski representable stack maps of a scheme morphism are the same data. Stated, rather than left implicit, because every transport below relies on it.

instance AlgebraicGeometry.representableFppfStackMap_isRepresentable {X Y : Scheme} (f : X ⟶ Y) : (representableFppfStackMap f).IsRepresentable

Every scheme-induced morphism of representable fppf stacks is representable, by the same fiber products as at the Zariski level.

theorem AlgebraicGeometry.representableFppfStackMap_hasRepresentableProperty (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderBaseChange] {X Y : Scheme} (f : X ⟶ Y) (hf : P f) : StackMorphism.HasRepresentableProperty P (representableFppfStackMap f)

A base-change-stable scheme-morphism property passes to the induced morphism of representable fppf stacks, checked on the actual representing scheme morphisms.

theorem AlgebraicGeometry.representableFppfStackMap_id_isSmoothSurjective (X : Scheme) : StackMorphism.IsSmoothSurjective (representableFppfStackMap (CategoryTheory.CategoryStruct.id X))

The identity atlas of a representable fppf stack is smooth and surjective on every representing scheme.

theorem AlgebraicGeometry.representableFppfStackMap_isLocallyOfFinitePresentation {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] : StackMorphism.IsLocallyOfFinitePresentation (representableFppfStackMap f)

A locally finitely presented scheme morphism induces a locally finitely presented morphism of representable fppf stacks.

theorem AlgebraicGeometry.representableFppfStackMap_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : StackMorphism.IsOpenImmersion (representableFppfStackMap f)

A scheme-theoretic open immersion induces an open immersion of representable fppf stacks.

instance AlgebraicGeometry.representableFppfStack_hasRepresentableDiagonal (X : Scheme) : StackInGroupoids.HasRepresentableDiagonal (representableFppfStack X)

The diagonal of a representable fppf stack is represented by the same scheme-theoretic equalizers as at the Zariski level.

Fppf presentations

structure AlgebraicGeometry.FppfStackPresentation : Type (u + 1)

Presentation data for a big-fppf stack: a representable diagonal, an atlas scheme, and an atlas whose every base change is an actual smooth-surjective scheme morphism.

Not called AlgebraicStack: the diagonal here is represented by schemes rather than by algebraic spaces, which is a different -- stronger -- condition than the standard definition asks for.

• toStackInGroupoids : CategoryTheory.StackInGroupoids Scheme Scheme.fppfTopology

  The underlying big-fppf stack in groupoids.

• schemeDiagonal : StackInGroupoids.HasRepresentableDiagonal self.toStackInGroupoids

  The diagonal is represented by schemes via its isomorphism functors.

• atlasScheme : Scheme

  The scheme presenting the stack.

• atlas : CategoryTheory.StackMorphism (representableFppfStack self.atlasScheme) self.toStackInGroupoids

  The atlas morphism from the corresponding representable fppf stack.

• atlasSmoothSurjective : StackMorphism.IsSmoothSurjective self.atlas

  Every base change of the atlas is an actual smooth-surjective scheme morphism.

def AlgebraicGeometry.representableFppfStackPresentation (X : Scheme) : FppfStackPresentation

Every representable big-fppf stack has an fppf presentation, using its identity atlas and its scheme-theoretic equalizer diagonal.

Equations

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

structure AlgebraicGeometry.FppfStackPresentationOver (S : Scheme) : Type (u + 1)

An fppf stack presentation locally of finite presentation over a base scheme, with local finite presentation checked on all scheme representatives of the structural morphism.

• toFppfStackPresentation : FppfStackPresentation

  The underlying fppf presentation.

• structureMorphism : CategoryTheory.StackMorphism self.toFppfStackPresentation.toStackInGroupoids (representableFppfStack S)

  Its structural morphism to the representable fppf stack of the base.

• locallyOfFinitePresentation : StackMorphism.IsLocallyOfFinitePresentation self.structureMorphism

  Local finite presentation, on every scheme representative.

def AlgebraicGeometry.representableFppfStackPresentationOver {X S : Scheme} (p : X ⟶ S) [LocallyOfFinitePresentation p] : FppfStackPresentationOver S

A locally finitely presented scheme morphism gives a locally finitely presented fppf presentation over its target.

Equations

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

noncomputable def AlgebraicGeometry.affineLineFppfStackPresentationOver (S : Scheme) : FppfStackPresentationOver S

A concrete positive-dimensional supported case at the fppf level: the representable affine-line stack has an fppf presentation locally of finite presentation over every base scheme.

This is the fppf counterpart of affineLineZariskiStackPresentationOver, and it is the reason the presentations above are inhabited by something other than a point.

Equations

• AlgebraicGeometry.affineLineFppfStackPresentationOver S = AlgebraicGeometry.representableFppfStackPresentationOver (AlgebraicGeometry.AffineSpace (ULift.{?u.1, 0} (Fin 1)) S ↘ S)