Theorems · Theorem · category theory

CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B B' : C} (p : B ⟶ B')
  (P : CategoryTheory.Functor (CategoryTheory.Over B')ᵒᵖ (Type w)) {X : CategoryTheory.Over B}
  (R : CategoryTheory.Sieve X) {X' : CategoryTheory.Over B'} (e : (CategoryTheory.Over.map p).obj X ≅ X'),
  CategoryTheory.Presieve.IsSheafFor ((CategoryTheory.Over.map p).op.comp P) R.arrows ↔
    CategoryTheory.Presieve.IsSheafFor P
      (CategoryTheory.Sieve.pullback e.inv
          (CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map p) R)).arrows

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category