Theorems · Definition · category theory
CategoryTheory.Over.left
{T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → CategoryTheory.Over X → TThe underlying object of an object in Over X.
- Defined in
- Mathlib.CategoryTheory.Comma.Over.Basic
- Cited by
- 541 results in Mathlib
- Foundations
- Depth 25 from the axioms, rests on 124 definitions · uses propext, Classical.choice, Quot.sound
- 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.Overstatement and proof · cited by 935
- CategoryTheory.Comma.leftproof · cited by 886
Cited by656
Results whose statement or proof uses this declaration.
- CategoryTheory.Over.homstatement · cited by 370
- CategoryTheory.Over.Hom.leftstatement · cited by 287
- CategoryTheory.Over.homMkstatement and proof · cited by 115
- CategoryTheory.GrothendieckTopology.overproof · cited by 115
- CategoryTheory.ChosenPullbacksAlong.pullbackObjproof · cited by 42
- CategoryTheory.Over.wstatement · cited by 42
- CategoryTheory.MonoOver.arrowstatement · cited by 41
- CategoryTheory.Presieve.categoryproof · cited by 38
- CategoryTheory.Sieve.overEquivstatement · cited by 28
- CategoryTheory.Over.OverMorphism.extstatement · cited by 27
- CategoryTheory.Presieve.coconestatement and proof · cited by 23
- CategoryTheory.Abelian.Preradical.rproof · cited by 23
Showing the 200 most cited of 656.