Theorems · Theorem · category theory
CategoryTheory.Presieve.isSheafFor_top
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
CategoryTheory.Presieve.IsSheafFor P ⊤Every presheaf is a sheaf for the maximal sieve. [Elephant] C2.1.5(ii)
- Defined in
- Mathlib.CategoryTheory.Sites.IsSheafFor
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Top.topstatement · cited by 9,680
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.CategoryStruct.idproof · cited by 6,235
- CategoryTheory.Sieveproof · cited by 552
- CategoryTheory.Presievestatement and proof · cited by 449
- CategoryTheory.Sieve.arrowsproof · cited by 446
- CategoryTheory.Presieve.IsSheafForstatement and proof · cited by 111
- CategoryTheory.Presieve.singletonproof · cited by 57
- CategoryTheory.Presieve.isSheafFor_iff_generateproof · cited by 20
- CategoryTheory.Sieve.arrows_topproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscreteproof · cited by 2
- CategoryTheory.Precoverage.isSheaf_toGrothendieck_iffproof · cited by 2
- CategoryTheory.Presieve.isSheafFor_top_sieveproof · cited by 0