Theorems · Theorem · category theory

CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {K : CategoryTheory.Precoverage C} [inst_2 : K.IsStableUnderBaseChange] {S : C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} {𝒰 : K.ZeroHypercover S} {𝒱 : K.ZeroHypercover S}
  (f : CategoryTheory.Precoverage.ZeroHypercover.Hom K 𝒰 𝒱),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f) →
    (∀ {X : C} (f : X ⟶ S),
        CategoryTheory.Presieve.IsSeparatedFor F
          (CategoryTheory.Presieve.ofArrows (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).X
            (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).f)) →
      CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒱.X 𝒱.f)

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.Precoverage.IsStableUnderBaseChange