Theorems · Theorem · category theory

CategoryTheory.CommSq.LiftStruct.fac_right

∀ {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} (self : sq.LiftStruct),
  CategoryTheory.CategoryStruct.comp self.l p = g

The lower right triangle commutes.

Defined in: Mathlib.CategoryTheory.CommSq
Cited by: 3 results in Mathlib
Foundations: Depth 5 from the axioms · uses no axioms
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

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
CategoryTheory.CommSqstatement and proof · cited by 158
CategoryTheory.CommSq.LiftStructstatement and proof · cited by 33
CategoryTheory.CommSq.LiftStruct.lstatement · cited by 10

Cited by3

Results whose statement or proof uses this declaration.

CategoryTheory.CommSq.fac_rightproof · cited by 19
CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zeroproof · cited by 2
CochainComplex.Lifting.hasLiftproof · cited by 0