Discrete stacks from sheaves of types

An ordinary sheaf of types on an arbitrary site determines a stack in discrete groupoids, and natural transformations induce stack morphisms through CategoryTheory.discretePseudofunctorMap and CategoryTheory.StackInGroupoids.discreteMap. This construction is purely site-theoretic; algebraic geometry consumes it for representable stacks.

def CategoryTheory.discretePseudofunctor {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat

Regard a presheaf of types as a pseudofunctor into discrete categories.

Equations

• CategoryTheory.discretePseudofunctor P = (P.comp CategoryTheory.typeToCat).toPseudofunctor'

def CategoryTheory.discretePseudofunctorMap {C : Type u} [Category.{v, u} C] {P Q : Functor Cᵒᵖ (Type w)} (φ : P ⟶ Q) : (discretePseudofunctor P).StrongTrans (discretePseudofunctor Q)

A natural transformation of presheaves induces a strong transformation between their discrete pseudofunctors. Its component functors apply the components of the original natural transformation directly.

Equations

• CategoryTheory.discretePseudofunctorMap φ = CategoryTheory.NatTrans.toStrongTrans (CategoryTheory.Functor.whiskerRight φ CategoryTheory.typeToCat)

instance CategoryTheory.discretePseudofunctor_obj_isDiscrete {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) (X : LocallyDiscrete Cᵒᵖ) : IsDiscrete ↑((discretePseudofunctor P).obj X)

instance CategoryTheory.discretePseudofunctor_obj_isGroupoid {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) (X : LocallyDiscrete Cᵒᵖ) : IsGroupoid ↑((discretePseudofunctor P).obj X)

theorem CategoryTheory.discretePseudofunctor_isStack {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} {J : GrothendieckTopology C} (hP : Presieve.IsSheaf J P) : (discretePseudofunctor P).IsStack J

A sheaf of types is a stack in discrete groupoids.

def CategoryTheory.stackInGroupoidsOfSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (P : Functor Cᵒᵖ (Type w)) (hP : Presieve.IsSheaf J P) : StackInGroupoids C J

Package a sheaf of types as a stack in discrete groupoids.

Equations

• CategoryTheory.stackInGroupoidsOfSheaf J P hP = { presheaf := CategoryTheory.discretePseudofunctor P, fiberIsGroupoid := ⋯, isStack := ⋯ }

theorem CategoryTheory.stackInGroupoidsOfSheaf_ofLE {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) (P : Functor Cᵒᵖ (Type w)) (hP : Presieve.IsSheaf J₂ P) : StackInGroupoids.ofLE h (stackInGroupoidsOfSheaf J₂ P hP) = stackInGroupoidsOfSheaf J₁ P ⋯

Restricting CategoryTheory.stackInGroupoidsOfSheaf to a coarser topology agrees with constructing its discrete stack from the restricted sheaf condition. This requires only a sheaf proof for the finer topology, with no representability or subcanonicity assumption.

def CategoryTheory.StackInGroupoids.discreteMap {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P Q : Functor Cᵒᵖ (Type w)} (hP : Presieve.IsSheaf J P) (hQ : Presieve.IsSheaf J Q) (φ : P ⟶ Q) : StackMorphism (stackInGroupoidsOfSheaf J P hP) (stackInGroupoidsOfSheaf J Q hQ)

A natural transformation between sheaves induces a morphism between the stacks supplied by CategoryTheory.stackInGroupoidsOfSheaf. This is CategoryTheory.discretePseudofunctorMap on their underlying pseudofunctors.

Equations

• CategoryTheory.StackInGroupoids.discreteMap hP hQ φ = CategoryTheory.discretePseudofunctorMap φ

@[simp]

theorem CategoryTheory.StackInGroupoids.discreteMap_app_obj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P Q : Functor Cᵒᵖ (Type w)} (hP : Presieve.IsSheaf J P) (hQ : Presieve.IsSheaf J Q) (φ : P ⟶ Q) (T : C) (x : P.obj (Opposite.op T)) : ((discreteMap hP hQ φ).app T).obj { as := x } = { as := (ConcreteCategory.hom (φ.app (Opposite.op T))) x }

The component functor of CategoryTheory.StackInGroupoids.discreteMap applies the underlying natural transformation to each object, definitionally.