Theorems · Definition · category theory
CategoryTheory.WideSubcategory.obj
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{_P : CategoryTheory.MorphismProperty C} → [inst_1 : _P.IsMultiplicative] → CategoryTheory.WideSubcategory _P → CThe category of which this is a wide subcategory
- Defined in
- Mathlib.CategoryTheory.Widesubcategory
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.MorphismProperty.IsMultiplicativestatement and proof · cited by 332
- CategoryTheory.WideSubcategorystatement and proof · cited by 26
Cited by25
Results whose statement or proof uses this declaration.
- CategoryTheory.WideSubcategory.isoMkstatement and proof · cited by 6
- CategoryTheory.wideSubcategoryInclusionproof · cited by 2
- CategoryTheory.WideSubcategory.extstatement and proof · cited by 1
- CategoryTheory.WideSubcategory.hom_extstatement · cited by 1
- CategoryTheory.WideSubcategory.rightUnitor_defstatement · cited by 0
- CategoryTheory.WideSubcategory.tensorHom_homstatement · cited by 0
- CategoryTheory.WideSubcategory.tensorObj_objstatement and proof · cited by 0
- CategoryTheory.WideSubcategory.tensorUnit_objstatement and proof · cited by 0
- CategoryTheory.WideSubcategory.tensorμ_homstatement · cited by 0
- CategoryTheory.WideSubcategory.whiskerLeft_homstatement · cited by 0
- CategoryTheory.WideSubcategory.whiskerRight_homstatement · cited by 0
- CategoryTheory.WideSubcategory.isoMk_inv_homstatement and proof · cited by 0