Representable stacks on subcanonical sites

A subcanonical topology makes every Yoneda presheaf a sheaf and hence a discrete stack.

Main definitions

• CategoryTheory.StackInGroupoids.representable constructs the stack represented by an object.
• CategoryTheory.StackInGroupoids.representableMap induces its maps by postcomposition.

Main results

• CategoryTheory.StackInGroupoids.representableMap_app_obj records the definitional action.
• CategoryTheory.StackInGroupoids.representable_ofLE identifies restriction to a coarser site.

Implementation notes

The construction reuses CategoryTheory.stackInGroupoidsOfSheaf: subcanonicity supplies its sheaf proof, rather than an additional descent hypothesis. Fibres currently lie in Cat.{v, v}, the universe of the Yoneda presheaf; #1637 will generalize this in place after #1631.

References

Mathlib's CategoryTheory/Sites/Canonical.lean supplies the represented-sheaf theorem. Stacks Project, Tag 0268 describes stacks by their fibre-to-descent-data equivalences, the condition carried by the existing sheaf-to-stack root.

Tags

subcanonical sites, representable stacks, discrete groupoids

def CategoryTheory.StackInGroupoids.representable {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) : StackInGroupoids C J

The stack represented by X on a subcanonical site is the discrete stack of yoneda.obj X, constructed by CategoryTheory.stackInGroupoidsOfSheaf.

Its fibres belong to Cat.{v, v} because yoneda.obj X is Type v-valued. After #1631, #1637 generalizes this construction in place to independent fibre universes, preserving the names CategoryTheory.StackInGroupoids.representable and CategoryTheory.StackInGroupoids.representableMap.

Equations

• CategoryTheory.StackInGroupoids.representable J X = CategoryTheory.stackInGroupoidsOfSheaf J (CategoryTheory.yoneda.obj X) ⋯

def CategoryTheory.StackInGroupoids.representableMap {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} (f : X ⟶ Y) : StackMorphism (representable J X) (representable J Y)

A morphism induces CategoryTheory.StackInGroupoids.representableMap by postcomposition on each fibre of the corresponding representable stacks.

Equations

• CategoryTheory.StackInGroupoids.representableMap J f = CategoryTheory.StackInGroupoids.discreteMap ⋯ ⋯ (CategoryTheory.yoneda.map f)

@[simp]

theorem CategoryTheory.StackInGroupoids.representableMap_app_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y T : C} (f : X ⟶ Y) (g : T ⟶ X) : ((representableMap J f).app T).obj { as := g } = { as := CategoryStruct.comp g f }

The component functors of CategoryTheory.StackInGroupoids.representableMap act by postcomposition, definitionally.

theorem CategoryTheory.StackInGroupoids.representable_ofLE {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} [J₁.Subcanonical] [J₂.Subcanonical] (h : J₁ ≤ J₂) (X : C) : ofLE h (representable J₂ X) = representable J₁ X

CategoryTheory.StackInGroupoids.representable is unchanged by restriction along an inequality between subcanonical topologies: CategoryTheory.StackInGroupoids.ofLE changes only its descent proof.