cocone_iso_of_hom_iso — Mathlib

English

A cocone morphism whose object part is an isomorphism is an isomorphism of cocones.

Русский

Кокон-морфизм, чья часть объектов является изоморфизмом, является изоморфизмом коконов.

LaTeX

$$cocone_iso_of_hom_iso {K : J ⥤ C} {c d : Cocone K} (f : c ⟶ d) [IsIso f.hom] : IsIso f$$

Lean4

/-- Given a cocone morphism whose object part is an isomorphism, produce an
isomorphism of cocones.
-/
theorem cocone_iso_of_hom_iso {K : J ⥤ C} {c d : Cocone K} (f : c ⟶ d) [i : IsIso f.hom] : IsIso f :=
  ⟨⟨{   hom := inv f.hom
        w := fun j => (asIso f.hom).comp_inv_eq.2 (f.w j).symm }, by cat_disch⟩⟩

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