Theorems · Definition · category theory
CategoryTheory.Arrow.right
{T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Arrow T → TThe right object of an arrow.
- Defined in
- Mathlib.CategoryTheory.Comma.Arrow
- Cited by
- 423 results in Mathlib
- Foundations
- Depth 12 from the axioms, rests on 46 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.Comma.rightproof · cited by 727
- CategoryTheory.Arrowstatement and proof · cited by 713
Cited by541
Results whose statement or proof uses this declaration.
- CategoryTheory.Arrow.homstatement · cited by 335
- CategoryTheory.Arrow.Hom.rightstatement · cited by 176
- CategoryTheory.Arrow.isoMkstatement and proof · cited by 53
- CategoryTheory.Arrow.homMkstatement and proof · cited by 35
- CategoryTheory.OrthogonalReflection.D₁.obj₂proof · cited by 31
- CategoryTheory.MorphismProperty.toSetproof · cited by 26
- CategoryTheory.Functor.mapArrowFunctorproof · cited by 23
- CategoryTheory.Limits.multicospanShapeEndproof · cited by 23
- CategoryTheory.Limits.multicospanIndexEndproof · cited by 22
- CategoryTheory.Arrow.hom_extstatement · cited by 21
- CategoryTheory.Limits.multispanShapeCoendproof · cited by 19
- CategoryTheory.OrthogonalReflection.D₂.multispanIndexproof · cited by 19
Showing the 200 most cited of 541.