Theorems · Definition · category theory
CategoryTheory.Presieve.category
{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Presieve X → Type (max u₁ v₁)The full subcategory of the over category C/X consisting of arrows which belong to a
presieve on X.
- Defined in
- Mathlib.CategoryTheory.Sites.Sieves
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 27 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.
Cites6
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.Overproof · cited by 935
- CategoryTheory.ObjectProperty.FullSubcategoryproof · cited by 726
- CategoryTheory.Over.leftproof · cited by 541
- CategoryTheory.Presievestatement and proof · cited by 449
- CategoryTheory.Over.homproof · cited by 370
Cited by62
Results whose statement or proof uses this declaration.
- CategoryTheory.Presieve.coconestatement · cited by 23
- CategoryTheory.Presieve.diagramstatement · cited by 17
- CategoryTheory.Presheaf.isSheaf_iff_isLimitstatement · cited by 6
- CategoryTheory.Sieve.ofArrows_category'statement and proof · cited by 6
- CategoryTheory.Sieve.exists_eq_ofArrowsproof · cited by 5
- CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimitstatement and proof · cited by 4
- CategoryTheory.Presieve.yonedaFamilyOfElements_fromCoconestatement · cited by 3
- CategoryTheory.Presieve.categoryMkstatement · cited by 3
- CategoryTheory.Presheaf.isLimit_iff_isSheafForstatement and proof · cited by 2
- CategoryTheory.Pseudofunctor.IsStackFor.isPrestackForproof · cited by 2
- CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheafproof · cited by 2
- CategoryTheory.Pseudofunctor.isPrestackFor_iffstatement and proof · cited by 2