Theorems · Definition · category theory
CategoryTheory.Over.star
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
(X : C) → [CategoryTheory.Limits.HasBinaryProducts C] → CategoryTheory.Functor C (CategoryTheory.Over X)The functor from C to Over X which sends Y : C to π₁ : X ⨯ Y ⟶ X, sometimes denoted X*.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound
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
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Functor.compproof · cited by 6,529
- CategoryTheory.Overstatement · cited by 935
- CategoryTheory.Limits.HasBinaryProductsstatement and proof · cited by 79
- CategoryTheory.prodComonadproof · cited by 20
- CategoryTheory.Comonad.cofreeproof · cited by 18
- CategoryTheory.coalgebraToOverproof · cited by 8
Cited by12
Results whose statement or proof uses this declaration.
- CategoryTheory.Over.starPullbackIsoStarstatement · cited by 2
- CategoryTheory.Over.forgetAdjStarstatement · cited by 2
- CategoryTheory.Over.starPullbackIsoStar_hom_app_leftstatement · cited by 0
- CategoryTheory.Over.starPullbackIsoStar_inv_app_leftstatement · cited by 0
- SheafOfModules.overPushforwardOverAdjstatement · cited by 0
- CategoryTheory.Over.star_map_leftstatement and proof · cited by 0
- CategoryTheory.Over.star_obj_homstatement and proof · cited by 0
- CategoryTheory.Over.star_obj_leftstatement and proof · cited by 0
- CategoryTheory.Over.forgetAdjStar_counit_appstatement · cited by 0
- SheafOfModules.pushforwardOverstatement · cited by 0
- CategoryTheory.Over.forgetAdjStar_unit_app_leftstatement · cited by 0
- CategoryTheory.GrothendieckTopology.coverPreserving_over_starstatement and proof · cited by 0