Theorems · Theorem · category theory

CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks

∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  (P : CategoryTheory.Functor Dᵒᵖ (Type u_2)) {X : C} (R : CategoryTheory.Presieve X) [R.HasPairwisePullbacks]
  [F.PreservesPairwisePullbacks R],
  CategoryTheory.Presieve.IsSheafFor (F.op.comp P) R ↔
    CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.map F R)

Defined in

Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Presieve.HasPairwisePullbacksCategoryTheory.Functor.PreservesPairwisePullbacks