Characterization of (pre)stacks for a precoverage

Let F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat be a pseudofunctor. Assuming F is a prestack for a Grothendieck topology J, we show that if f : X i ⟶ S and f' : X' j ⟶ S are two covering families of morphisms in S such that the sieve generated by f' is contained in the sieve generated by f, then the functor F.DescentData f ⥤ F.DescentData f' is fully faithful. It follows that if the descent is effective for the family f', then it is also effective for the family f. We translate this result in terms of the predicate IsStackFor as the lemma IsStackFor.of_le: if R ≤ R' is an inequality of presieves where R is covering, then F.IsStackFor R implies F.IsStackFor R'.

Now, assume that J is a precoverage on C which satisfies slightly stronger axioms than pretopologies (J.HasIsos, J.IsStableUnderBaseChange, and J.IsStableUnderComposition). We deduce from the results above that F is a prestack (resp. a stack) for the Grothendieck topology associated to J if F satisfies F.IsPrestackFor R (resp. F.IsStackFor R) for the presieves R that are part of J.

theorem CategoryTheory.Pseudofunctor.DescentData.faithful_pullFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = f' j) (hf' : Sieve.ofArrows X' f' ∈ J S) : (pullFunctor F ⋯).Faithful

theorem CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = f' j) (hf' : Sieve.ofArrows X' f' ∈ J S) : (pullFunctor F ⋯).Full

noncomputable def CategoryTheory.Pseudofunctor.DescentData.fullyFaithfulPullFunctor {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryStruct.comp (p' j) (f (α j)) = f' j) (hf' : Sieve.ofArrows X' f' ∈ J S) : (pullFunctor F ⋯).FullyFaithful

Let F be a prestack for a Grothendieck topology J, f : X i ⟶ S and f' : X' j ⟶ S be two families of morphisms. Assume that f' is a covering family for J, then functors F.pullFunctor .. : F.DescentData f ⥤ F.DescentData f' are fully faithful.

theorem CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {J : GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} (h₁ : Sieve.ofArrows X' f' ∈ J S) (h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f) [(F.toDescentData f').IsEquivalence] : (F.toDescentData f).IsEquivalence

theorem CategoryTheory.Pseudofunctor.IsStackFor.of_le {C : Type u} [Category.{v, u} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) {S : C} {R : Presieve S} (hR₁ : F.IsStackFor R) {J : GrothendieckTopology C} (hR₂ : Sieve.generate R ∈ J S) [F.IsPrestack J] {R' : Presieve S} (h : R ≤ R') : F.IsStackFor R'

If F is a prestack for a Grothendieck topology J and F is a stack for a covering presieve R, then it is also a stack for R' if R ≤ R'.

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

If F is a prestack for a Grothendieck topology J and F is a stack for a covering sieve R, then it is also a stack for R' if R ≤ R'.

theorem CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} [Limits.HasPullbacks C] {J : Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R) : F.IsPrestack J.toGrothendieck

If a precoverage satisfies HasIsos, IsStableUnderBaseChange and IsStableUnderComposition (which is a slightly stronger condition as compared to pretopologies), then in order to check that a pseudofunctor is a prestack it suffices to check that it is a prestack for the presieves that are part of the precoverage.

theorem CategoryTheory.Pseudofunctor.IsStack.of_precoverage {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} [Limits.HasPullbacks C] {J : Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R) : F.IsStack J.toGrothendieck

If a precoverage satisfies HasIsos, IsStableUnderBaseChange and IsStableUnderComposition (which is a slightly stronger condition as compared to pretopologies), then in order to check that a pseudofunctor is a stack it suffices to check that it is a stack for the presieves that are part of the precoverage.