isomorphisms — Mathlib

English

Isomorphisms form a morphism property stable under retracts.

Русский

Изоморфизмы образуют свойство морфизмов, устойчивое к retracts.

LaTeX

$$(isomorphisms C).IsStableUnderRetracts$$

Lean4

instance isomorphisms : (isomorphisms C).IsStableUnderRetracts where
  of_retract {X Y Z W f g} h
    (_ : IsIso _) := by
    refine ⟨h.i.right ≫ inv g ≫ h.r.left, ?_, ?_⟩
    · rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]
    · rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]

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