Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ J X ↔ CategoryTheory.Presieve.IsSheafFor (CategoryTheory.Functor.closedSieves J).toFunctor S.arrows

A sieve S is covering for J if and only if the subobject classifier is a sheaf for S.

Defined in

Mathlib.CategoryTheory.Sites.Closed

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category