Theorems · Theorem · category theory

CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')}
  (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)),
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)),
      e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) =
        (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) →
    (CategoryTheory.Presieve.IsSheaf J P₁ ↔ CategoryTheory.Presieve.IsSheaf J P₂)

Defined in

Mathlib.CategoryTheory.Sites.SheafOfTypes

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category