Representable stacks on the big scheme sites

The generic construction of a discrete stack from a sheaf and the generic notion of a representable stack morphism are owned by CategoryTheory/Sites/Descent/StackInGroupoids. This geometric consumer applies that API to the subcanonical big-Zariski, fppf and étale sites of schemes. The slice-site example below uses Mathlib’s subcanonical-over instance.

@[reducible, inline]

abbrev AlgebraicGeometry.representableZariskiStack (X : Scheme) : CategoryTheory.StackInGroupoids Scheme Scheme.zariskiTopology

The big-Zariski stack represented by a scheme X.

Equations

• AlgebraicGeometry.representableZariskiStack X = CategoryTheory.StackInGroupoids.representable AlgebraicGeometry.Scheme.zariskiTopology X

@[reducible, inline]

abbrev AlgebraicGeometry.representableFppfStack (X : Scheme) : CategoryTheory.StackInGroupoids Scheme Scheme.fppfTopology

The big-fppf stack represented by a scheme X. Its subcanonicity follows from fpqc descent for representable presheaves.

Equations

• AlgebraicGeometry.representableFppfStack X = CategoryTheory.StackInGroupoids.representable AlgebraicGeometry.Scheme.fppfTopology X

@[reducible, inline]

abbrev AlgebraicGeometry.representableEtaleStack (X : Scheme) : CategoryTheory.StackInGroupoids Scheme Scheme.etaleTopology

The big-étale stack represented by a scheme X.

Equations

• AlgebraicGeometry.representableEtaleStack X = CategoryTheory.StackInGroupoids.representable AlgebraicGeometry.Scheme.etaleTopology X

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

The stack represented by X has effective Čech descent for every big Zariski covering family.

Equations

• AlgebraicGeometry.representableZariskiCechDescentEquivalence X S U = (AlgebraicGeometry.representableZariskiStack X).cechDescentEquivalence U

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

A morphism T ⟶ X, regarded as an object of the stack represented by X over T.

Equations

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

theorem AlgebraicGeometry.representableZariskiObject_injective {X T : Scheme} : Function.Injective representableZariskiObject

The representable stack remembers its scheme morphisms faithfully.