Theorems · Definition · category theory
CategoryTheory.CommSq.lift
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
{A B X Y : C} →
{f : A ⟶ X} →
{i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → (sq : CategoryTheory.CommSq f i p g) → [hsq : sq.HasLift] → B ⟶ XA choice of a diagonal morphism that is part of a LiftStruct when
the square has a lift.
- Defined in
- Mathlib.CategoryTheory.CommSq
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Nonempty.someproof · cited by 340
- CategoryTheory.CommSqstatement and proof · cited by 158
- CategoryTheory.CommSq.HasLiftstatement and proof · cited by 20
- CategoryTheory.CommSq.LiftStruct.lproof · cited by 10
- CategoryTheory.CommSq.HasLift.exists_liftproof · cited by 4
Cited by40
Results whose statement or proof uses this declaration.
- CategoryTheory.CommSq.fac_leftstatement · cited by 22
- CategoryTheory.CommSq.fac_rightstatement · cited by 19
- CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImageproof · cited by 9
- CategoryTheory.CommSq.fac_right_assocstatement and proof · cited by 3
- CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'proof · cited by 3
- HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObjectproof · cited by 3
- SSet.horn.IsCompatible.exists_liftproof · cited by 3
- CategoryTheory.CommSq.fac_left_assocstatement and proof · cited by 2
- SSet.quasicategory_of_hasLiftingPropertyproof · cited by 2
- HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinderproof · cited by 2