Theorems · Definition · category theory
CategoryTheory.Under
{T : Type u₁} → [CategoryTheory.Category.{v₁, u₁} T] → T → Type (max u₁ v₁)The under category has as objects arrows with domain X and as morphisms commutative
triangles.
- Defined in
- Mathlib.CategoryTheory.Comma.Over.Basic
- Cited by
- 276 results in Mathlib
- Foundations
- Depth 24 from the axioms, rests on 122 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.Functor.idproof · cited by 3,333
- CategoryTheory.StructuredArrowproof · cited by 370
Cited by388
Results whose statement or proof uses this declaration.
- CategoryTheory.Under.rightstatement and proof · cited by 128
- CategoryTheory.Under.forgetstatement · cited by 90
- CategoryTheory.Under.homstatement and proof · cited by 73
- CategoryTheory.Under.Hom.rightstatement and proof · cited by 67
- CategoryTheory.Under.mkstatement · cited by 65
- CategoryTheory.Under.homMkstatement and proof · cited by 43
- CategoryTheory.Under.mapstatement · cited by 32
- CategoryTheory.Under.poststatement and proof · cited by 24
- CommRingCat.mkUnderstatement · cited by 24
- CategoryTheory.Under.pushoutstatement and proof · cited by 21
- CategoryTheory.WithInitial.liftFromUnderstatement · cited by 21
- CategoryTheory.WithInitial.coconeEquivstatement and proof · cited by 16
Showing the 200 most cited of 388.