instIsIsoIndCoimageImageComparison

English

In an abelian context for Ind-objects, the canonical coimage-to-image morphism coimage(f) → image(f) is an isomorphism.

Русский

В абелевой обстановке для объектов-индуктов канонический морфизм coimage(f) → image(f) является изоморфизмом.

LaTeX

$$$\\operatorname{coimage}(f) \\cong \\operatorname{image}(f)$$$

Lean4

instance {X Y : Ind C} (f : X ⟶ Y) : IsIso (Abelian.coimageImageComparison f) :=
  by
  obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)
  let i' := coimageImageComparisonFunctor.mapIso i
  dsimp only [coimageImageComparisonFunctor_obj, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom] at i'
  have := Iso.isIso_hom i'
  rw [Arrow.isIso_iff_isIso_of_isIso i'.hom,
    Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]
  infer_instance

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