cone_iso_of_hom_iso — Mathlib

English

If a cone morphism f has an isomorphism on its object part, then f is an isomorphism of cones.

Русский

Если конусный мороморфизм f имеет изоморфизм на части объекта, то f является изоморфизмом конусов.

LaTeX

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

Lean4

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

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