Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.IsStack.of_precoverage

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange]
  [J.IsStableUnderComposition], (∀ (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.

Defined in

Mathlib.CategoryTheory.Sites.Descent.Precoverage

Cited by

0 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.Precoverage.HasIsosCategoryTheory.Precoverage.IsStableUnderBaseChangeCategoryTheory.Precoverage.IsStableUnderComposition