FGModuleCat K is an abelian category.

instance FGModuleCat.instIsIsoCoimageImageComparison {k : Type u} [Ring k] [IsNoetherianRing k] {X Y : FGModuleCat k} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)

@[instance_reducible]

instance FGModuleCat.instAbelian {k : Type u} [Ring k] [IsNoetherianRing k] : CategoryTheory.Abelian (FGModuleCat k)

Equations

• FGModuleCat.instAbelian = CategoryTheory.Abelian.ofCoimageImageComparisonIsIso