Theorems · Definition · category theory
CategoryTheory.MonoOver.arrow
{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → (f : CategoryTheory.MonoOver X) → f.obj.left ⟶ XConvenience notation for the underlying arrow of a monomorphism over X.
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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.Homstatement · cited by 32,603
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
- CategoryTheory.Overstatement · cited by 935
- CategoryTheory.Over.leftstatement · cited by 541
- CategoryTheory.Over.homproof · cited by 370
- CategoryTheory.MonoOverstatement and proof · cited by 115
- CategoryTheory.Over.isMonostatement · cited by 111
Cited by58
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoOver.homMkstatement and proof · cited by 18
- CategoryTheory.MonoOver.isoMkstatement and proof · cited by 9
- CategoryTheory.Subfunctor.equivalenceMonoOverproof · cited by 8
- CategoryTheory.Subobject.indproof · cited by 7
- CategoryTheory.Subobject.liftproof · cited by 6
- CategoryTheory.Subobject.factors_of_leproof · cited by 5
- CategoryTheory.MonoOver.Factorsproof · cited by 4
- CategoryTheory.MonoOver.wstatement · cited by 3
- CategoryTheory.Subobject.inf_eq_map_pullback'statement · cited by 3
- CategoryTheory.MonoOver.bot_arrow_eq_zerostatement and proof · cited by 2
- CategoryTheory.MonoOver.infproof · cited by 2
- CategoryTheory.Subobject.factors_of_factors_rightproof · cited by 2