Theorems · Theorem · category theory
CategoryTheory.CommSq.fac_left
∀ {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], CategoryTheory.CategoryStruct.comp i sq.lift = f- Defined in
- Mathlib.CategoryTheory.CommSq
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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.CategoryStruct.compstatement · cited by 17,999
- Nonempty.someproof · cited by 340
- CategoryTheory.CommSqstatement and proof · cited by 158
- CategoryTheory.CommSq.liftstatement · cited by 34
- CategoryTheory.CommSq.HasLiftstatement and proof · cited by 20
- CategoryTheory.CommSq.HasLift.exists_liftproof · cited by 4
- CategoryTheory.CommSq.LiftStruct.fac_leftproof · cited by 3
Cited by22
Results whose statement or proof uses this declaration.
- CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'proof · cited by 3
- SSet.horn.IsCompatible.exists_liftproof · cited by 3
- SSet.quasicategory_of_hasLiftingPropertyproof · cited by 2
- CategoryTheory.CommSq.fac_left_assocproof · cited by 2
- HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinderproof · cited by 2
- CategoryTheory.CommSq.HasLift.overproof · cited by 1
- HomotopicalAlgebra.CofibrantObject.exists_bifibrant_mapproof · cited by 1
- HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution_mapproof · cited by 1
- CategoryTheory.isIso_of_epi_of_strongMonoproof · cited by 1
- CategoryTheory.isIso_of_mono_of_strongEpiproof · cited by 1