instIsIsoCoimageImageComparison — Mathlib

English

For a morphism f in FGModuleCat over Noetherian ring k, the coimage-image comparison is an isomorphism.

Русский

Для морфизма f в FGModuleCat над кольцом k, удовлетворяющим условию Нотер, сопоставление кообраз-образ является изоморфизмом.

LaTeX

$$$\\mathrm{Abelian.coimageImageComparison}(f) \\; \\text{is an isomorphism}$$$

Lean4

instance {X Y : FGModuleCat k} (f : X ⟶ Y) : IsIso (Abelian.coimageImageComparison f) :=
  have :=
    IsIso.of_isIso_fac_right
      (Abelian.PreservesCoimage.hom_coimageImageComparison (forget₂ (FGModuleCat k) (ModuleCat k)) f).symm
  Functor.FullyFaithful.isIso_of_isIso_map (ModuleCat.isFG k).fullyFaithfulι _

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