Theorems · Definition · category theory
CategoryTheory.Arrow.left
{T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Arrow T → TThe left object of an arrow.
- Defined in
- Mathlib.CategoryTheory.Comma.Arrow
- Cited by
- 426 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.leftproof · cited by 886
- 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.leftstatement · cited by 160
- CategoryTheory.Arrow.isoMkstatement and proof · cited by 53
- CategoryTheory.OrthogonalReflection.D₁proof · cited by 35
- CategoryTheory.Arrow.homMkstatement and proof · cited by 35
- CategoryTheory.OrthogonalReflection.D₁.obj₁proof · cited by 33
- CategoryTheory.MorphismProperty.toSetproof · cited by 26
- CategoryTheory.Functor.mapArrowFunctorproof · cited by 23
- CategoryTheory.Limits.multicospanShapeEndproof · cited by 23
- CategoryTheory.SmallObject.objproof · cited by 22
- CategoryTheory.Limits.multicospanIndexEndproof · cited by 22
- CategoryTheory.Arrow.hom_extstatement · cited by 21
Showing the 200 most cited of 541.