rightLiftingProperty — Mathlib

English

If f' → f is a retract and g has a lifting with f, then g has a lifting with f'.

Русский

Если f' → f образуют retract и g имеет подъём по отношению к f, то g имеет подъём по отношению к f'.

LaTeX

$$$$ \\text{If } h:\\mathrm{RetractArrow}(f',f) \\text{ and } HasLiftingProperty\, g\, f \\text{ then } HasLiftingProperty\, g\, f' $$$$

Lean4

theorem rightLiftingProperty {X Y Z W X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (h : RetractArrow f' f) (g : Z ⟶ W)
    [HasLiftingProperty g f] : HasLiftingProperty g f' where
  sq_hasLift := fun {u v} sq ↦
    have sq' : CommSq (u ≫ h.i.left) g f (v ≫ h.i.right) :=
      ⟨by rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]⟩
    ⟨⟨{ l := sq'.lift ≫ h.r.left }⟩⟩

Похожие утверждения