Theorems · Definition · category theory
CategoryTheory.Limits.HasPullbacksAlong
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → PropHasPullbacksAlong f states that pullbacks of all morphisms into Y
along f : X ⟶ Y exist.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 18 from the axioms · 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
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Limits.HasPullbackproof · cited by 434
Cited by27
Results whose statement or proof uses this declaration.
- CategoryTheory.Over.pullbackstatement and proof · cited by 53
- CategoryTheory.Over.pullback_map_leftstatement and proof · cited by 9
- CategoryTheory.Over.mapPullbackAdjstatement and proof · cited by 8
- CategoryTheory.IsPullback.isoOverPullbackstatement and proof · cited by 4
- CategoryTheory.IsPullback.isoOverPullback_hom_left_comp_sndstatement and proof · cited by 2
- CategoryTheory.MorphismProperty.Over.pullbackCompForgetIsostatement and proof · cited by 2
- CategoryTheory.Limits.hasPullback_symmetry_of_hasPullbacksAlongstatement and proof · cited by 2
- CategoryTheory.MorphismProperty.overPullbackMapstatement and proof · cited by 2
- CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlongstatement and proof · cited by 2
- CategoryTheory.Over.mapPullbackAdj_counit_appstatement and proof · cited by 2
- CategoryTheory.MorphismProperty.pullbackMapstatement and proof · cited by 1
- CategoryTheory.IsPullback.of_over_isostatement and proof · cited by 1