Theorems · Theorem · category theory

CategoryTheory.Presieve.IsSheaf.isSheafFor

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presieve.IsSheaf J P →
    ∀ (R : CategoryTheory.Presieve X), CategoryTheory.Sieve.generate R ∈ J X → CategoryTheory.Presieve.IsSheafFor P R

Defined in

Mathlib.CategoryTheory.Sites.SheafOfTypes

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category