Theorems · Theorem · category theory
CategoryTheory.CommSq.fac_right
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : X ⟶ A} {i : B ⟶ A} {p : Y ⟶ X}
{g : Y ⟶ B} (sq : CategoryTheory.CommSq g p i f) [hsq : sq.HasLift], CategoryTheory.CategoryStruct.comp sq.lift i = f- Defined in
- Mathlib.CategoryTheory.CommSq
- Cited by
- 19 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_rightproof · cited by 3
Cited by19
Results whose statement or proof uses this declaration.
- CategoryTheory.CommSq.fac_right_assocproof · cited by 3
- CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'proof · cited by 3
- SSet.horn.IsCompatible.exists_liftproof · cited by 3
- CategoryTheory.CommSq.HasLift.overproof · cited by 1
- HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution_mapproof · cited by 1
- CategoryTheory.projective_iff_llp_epimorphisms_of_isZeroproof · cited by 1
- CategoryTheory.isIso_of_epi_of_strongMonoproof · cited by 1
- CategoryTheory.isIso_of_mono_of_strongEpiproof · cited by 1
- HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extensionproof · cited by 0
- CategoryTheory.strongEpi_of_strongEpiproof · cited by 0