Theorems · Theorem · category theory

CategoryTheory.Presieve.isSheafFor_over_map_op_comp_ofArrows_iff

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {B B' : C} (p : B ⟶ B')
  (P : CategoryTheory.Functor (CategoryTheory.Over B')ᵒᵖ (Type w)) {X : CategoryTheory.Over B}
  {Y : I → CategoryTheory.Over B} (f : (i : I) → Y i ⟶ X),
  CategoryTheory.Presieve.IsSheafFor ((CategoryTheory.Over.map p).op.comp P) (CategoryTheory.Presieve.ofArrows Y f) ↔
    CategoryTheory.Presieve.IsSheafFor P
      (CategoryTheory.Presieve.ofArrows (fun i => (CategoryTheory.Over.map p).obj (Y i)) fun i =>
        (CategoryTheory.Over.map p).map (f i))

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category