English
If g' → g is a retract and f has a lifting with g, then g' also has a lifting with f.
Русский
Если g' → g образуют retract, и f имеет подъём по отношению к g, то и g' имеет подъём по отношению к f.
LaTeX
$$$$ \\text{If } h:\\mathrm{RetractArrow}(g',g) \\text{ and } HasLiftingProperty\, g\, f \\text{ then } HasLiftingProperty\, g'\\, f $$$$
Lean4
theorem leftLiftingProperty {X Y Z W Z' W' : C} {g : Z ⟶ W} {g' : Z' ⟶ W'} (h : RetractArrow g' g) (f : X ⟶ Y)
[HasLiftingProperty g f] : HasLiftingProperty g' f where
sq_hasLift := fun {u v} sq ↦
by
have sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v) := by
simp only [Arrow.mk_left, Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]
exact ⟨⟨{
l := h.i.right ≫ sq'.lift
fac_left := by
simp only [← h.i_w_assoc, sq'.fac_left, h.retract_left_assoc, Arrow.mk_left, Category.id_comp] }⟩⟩
