Theorems · Definition · category theory
CategoryTheory.Presieve
{C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max u₁ v₁)A predicate on arrows with codomain X.
- Defined in
- Mathlib.CategoryTheory.Sites.Sieves
- Cited by
- 449 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 7 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- Quiver.Homproof · cited by 32,603
Cited by656
Results whose statement or proof uses this declaration.
- CategoryTheory.Sieve.arrowsstatement · cited by 446
- CategoryTheory.Precoverage.coveringsstatement · cited by 194
- CategoryTheory.Presieve.ofArrowsstatement · cited by 150
- CategoryTheory.Sieve.generatestatement and proof · cited by 117
- CategoryTheory.Presieve.IsSheafForstatement and proof · cited by 111
- CategoryTheory.Presieve.FamilyOfElementsstatement and proof · cited by 103
- CategoryTheory.Presieve.FamilyOfElements.Compatiblestatement and proof · cited by 79
- CategoryTheory.PreZeroHypercover.presieve₀statement · cited by 70
- CategoryTheory.Presieve.singletonstatement · cited by 57
- CategoryTheory.Presieve.FamilyOfElements.IsAmalgamationstatement and proof · cited by 53
- CategoryTheory.Presieve.categorystatement and proof · cited by 38
- CategoryTheory.Presieve.mapstatement · cited by 38
Showing the 200 most cited of 656.