Theorems · Definition · category theory
CategoryTheory.ObjectProperty.FullSubcategory.obj
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {P : CategoryTheory.ObjectProperty C} → P.FullSubcategory → CThe category of which this is a full subcategory
- Cited by
- 1,316 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 6 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.ObjectProperty.FullSubcategorystatement and proof · cited by 726
Cited by1,673
Results whose statement or proof uses this declaration.
- CategoryTheory.Subobject.arrowproof · cited by 175
- CategoryTheory.ObjectProperty.ιproof · cited by 95
- TopCat.Sheaf.presheafproof · cited by 79
- CategoryTheory.ObjectProperty.FullSubcategory.propertystatement · cited by 76
- CategoryTheory.ObjectProperty.homMkstatement and proof · cited by 71
- SheafOfModules.valstatement · cited by 55
- SheafOfModules.unitproof · cited by 45
- CategoryTheory.sheafifyproof · cited by 44
- CategoryTheory.MonoOver.arrowstatement and proof · cited by 41
- SheafOfModules.Hom.valstatement · cited by 39
- FintypeCat.toProfiniteproof · cited by 32
- FGModuleCat.carrierproof · cited by 28
Showing the 200 most cited of 1,673.