Stacks: effectiveness of descent

Let C be a category with a Grothendieck topology J and F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat. In this file, we define the typeclass F.IsStack J saying that F is a stack for J. (See the terminological note in the file Sites.Descent.IsPrestack: we do not require that the categories F.obj (.mk (op S)) are groupoids.)

The typeclass IsStack extends IsPrestack. The effectiveness of descent that is required for stacks is expressed by saying that the functors toDescentData attached to covering sieves are essentially surjective. Together with the IsPrestack assumption, we get that these functors are actually equivalences of categories (see isEquivalence_toDescentData). Conversely, we provide a constructor IsStack.of_isStackFor which assumes that these functors are equivalences of categories.

References

• Jean Giraud, Cohomologie non abélienne
• Gérard Laumon and Laurent Moret-Bailly, Champs algébriques

class CategoryTheory.Pseudofunctor.IsStack {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) (J : GrothendieckTopology C) extends F.IsPrestack J : Prop

The property that a pseudofunctor F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat has effective descent for a Grothendieck topology, i.e. is a stack. (See the terminological note in the introduction of the file Sites.Descent.IsPrestack.)

• isSheaf {S : C} (M N : ↑(F.obj { as := Opposite.op S })) : Presheaf.IsSheaf (J.over S) (F.presheafHom M N)
• essSurj_of_sieve {S : C} (R : Sieve S) (hR : R ∈ J S) : (F.toDescentData fun (f : R.arrows.category) => f.obj.hom).EssSurj

theorem CategoryTheory.Pseudofunctor.isStackFor' {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsStack J] {S : C} (R : Sieve S) (hR : R ∈ J S) : F.IsStackFor R.arrows

Version of isStackFor for a sieve instead of a presieve.

theorem CategoryTheory.Pseudofunctor.isStackFor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsStack J] {S : C} (R : Presieve S) (hR : Sieve.generate R ∈ J S) : F.IsStackFor R

theorem CategoryTheory.Pseudofunctor.isEquivalence_toDescentData {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsStack J] {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hf : Sieve.ofArrows X f ∈ J S) : (F.toDescentData f).IsEquivalence

theorem CategoryTheory.Pseudofunctor.IsStack.of_isStackFor {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {J : GrothendieckTopology C} (hF : ∀ (S : C), ∀ R ∈ J S, F.IsStackFor R.arrows) : F.IsStack J