of_right_iso — Mathlib

English

Isomorphisms are lifting against any morphism.

Русский

Изоморфизмы поднимаются над любыми морфизмами.

LaTeX

$$$$ HasLiftingProperty\\big(i\\,,p\\big) \\text{ for any } p \\text{ when } i \\text{ is an isomorphism} $$$$

Lean4

instance (priority := 100) of_right_iso [IsIso p] : HasLiftingProperty i p :=
  ⟨fun {f} {g} sq =>
    CommSq.HasLift.mk'
      { l := g ≫ inv p
        fac_left := by simp only [← sq.w_assoc, IsIso.hom_inv_id, comp_id]
        fac_right := by simp only [assoc, IsIso.inv_hom_id, comp_id] }⟩

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