Theorems · Inductive type · category theory
CategoryTheory.CommSq.HasLift
{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} → CategoryTheory.CommSq f i p g → PropThe assertion that a square has a LiftStruct.
- Defined in
- Mathlib.CategoryTheory.CommSq
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 3 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 · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.CommSqstatement · cited by 158
Cited by29
Results whose statement or proof uses this declaration.
- CategoryTheory.CommSq.liftstatement and proof · cited by 34
- CategoryTheory.CommSq.fac_leftstatement and proof · cited by 22
- CategoryTheory.CommSq.fac_rightstatement and proof · cited by 19
- AlgebraicGeometry.ValuativeCriterion.Existenceproof · cited by 11
- CategoryTheory.CommSq.HasLift.exists_liftstatement and proof · cited by 4
- CategoryTheory.CommSq.fac_right_assocstatement and proof · cited by 3
- CategoryTheory.CommSq.HasLift.iffstatement and proof · cited by 3
- CategoryTheory.CommSq.HasLift.mk'statement · cited by 3
- AlgebraicGeometry.ValuativeCriterion.iffproof · cited by 3
- CategoryTheory.CommSq.fac_left_assocstatement and proof · cited by 2
- CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftstatement · cited by 2
- CategoryTheory.HasLiftingPropertyFixedBotproof · cited by 2