of_left_iso — Mathlib

English

If i is an isomorphism, then i has the lifting property against any p.

Русский

Если i является изоморфизмом, то против любого p у i есть свойство подъёма.

LaTeX

$$$$ [IsIso\, i] \\Rightarrow HasLiftingProperty\, i\, p $$$$

Lean4

instance (priority := 100) of_left_iso [IsIso i] : HasLiftingProperty i p :=
  ⟨fun {f} {g} sq =>
    CommSq.HasLift.mk'
      { l := inv i ≫ f
        fac_left := by simp only [IsIso.hom_inv_id_assoc]
        fac_right := by simp only [sq.w, assoc, IsIso.inv_hom_id_assoc] }⟩

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