functor_category_isIso_coimageImageComparison

English

The coimage-image comparison transformation is an isomorphism in the abelian setting.

Русский

Преобразование сопоставления кообразования и образа является изоморфизмом в абелевой обстановке.

LaTeX

$$$\mathrm{IsIso}(\mathrm{coimageImageComparison}(\alpha))$$$

Lean4

instance functor_category_isIso_coimageImageComparison : IsIso (Abelian.coimageImageComparison α) :=
  by
  have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) :=
    by
    intros
    rw [coimageImageComparison_app']
    infer_instance
  apply NatIso.isIso_of_isIso_app

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