The category of finitely generated modules over a Noetherian ring is abelian.

This file is basically a copy of Algebra/ModuleCat/Abelian.lean

noncomputable def FGModuleCat.normalMono {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) (hf : CategoryTheory.Mono f) : CategoryTheory.NormalMono f

A monomorphism between finitely generated modules is a normal monomorphism

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FGModuleCat.normalEpi {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) (hf : CategoryTheory.Epi f) : CategoryTheory.NormalEpi f

An epimorphism between finitely generated modules is a normal epimorphism

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance FGModuleCat.abelian_of_noetherian {R : Type u} [CommRing R] [IsNoetherianRing R] : CategoryTheory.Abelian (FGModuleCat R)

Equations

• FGModuleCat.abelian_of_noetherian = CategoryTheory.Abelian.mk

instance FGModuleCat.instHasForget₂Ab_hilbertPolynomial {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (FGModuleCat R) Ab

Equations

• One or more equations did not get rendered due to their size.

instance FGModuleCat.instAdditiveAbForget₂_hilbertPolynomial {R : Type u} [CommRing R] : (CategoryTheory.forget₂ (FGModuleCat R) Ab).Additive

instance FGModuleCat.instPreservesFiniteLimitsAbForget₂_hilbertPolynomial {R : Type u} [CommRing R] [IsNoetherianRing R] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FGModuleCat R) Ab)

instance FGModuleCat.instPreservesFiniteLimitsForget_hilbertPolynomial {R : Type u} [CommRing R] [IsNoetherianRing R] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget (FGModuleCat R))

instance FGModuleCat.instPreservesLimitsOfShapeWalkingCospanForget_hilbertPolynomial {R : Type u} [CommRing R] [IsNoetherianRing R] : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget (FGModuleCat R))

noncomputable def FGModuleCat.imageFactorisation {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.ImageFactorisation f

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FGModuleCat.imageFactorisation_F_m {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) : (imageFactorisation f).F.m = ofHom (LinearMap.range (ModuleCat.Hom.hom f)).subtype

@[simp]

theorem FGModuleCat.imageFactorisation_isImage_lift {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) (F : CategoryTheory.Limits.MonoFactorisation f) : (imageFactorisation f).isImage.lift F = ofHom { toFun := fun (x : ↥(LinearMap.range (ModuleCat.Hom.hom f))) => (CategoryTheory.ConcreteCategory.hom F.e) (Exists.choose ⋯), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem FGModuleCat.imageFactorisation_F_I_obj_carrier {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) : ↑(imageFactorisation f).F.I.obj = ↥(LinearMap.range (ModuleCat.Hom.hom f))

@[simp]

theorem FGModuleCat.imageFactorisation_F_e {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) : (imageFactorisation f).F.e = ofHom (ModuleCat.Hom.hom f).rangeRestrict

@[simp]

theorem FGModuleCat.imageFactorisation_F_I_obj_isModule {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) : (imageFactorisation f).F.I.obj.isModule = (LinearMap.range (ModuleCat.Hom.hom f)).module

@[simp]

theorem FGModuleCat.imageFactorisation_F_I_obj_isAddCommGroup {R : Type u} [CommRing R] [IsNoetherianRing R] {M N : FGModuleCat R} (f : M ⟶ N) : (imageFactorisation f).F.I.obj.isAddCommGroup = (LinearMap.range (ModuleCat.Hom.hom f)).addCommGroup

instance FGModuleCat.hasImages_fgModuleCat {R : Type u} [CommRing R] [IsNoetherianRing R] : CategoryTheory.Limits.HasImages (FGModuleCat R)

noncomputable def FGModuleCat.imageIsoRange {R : Type u} [CommRing R] [IsNoetherianRing R] {G H : FGModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.image f ≅ of R ↥(LinearMap.range (ModuleCat.Hom.hom f))

Equations

• FGModuleCat.imageIsoRange f = (CategoryTheory.Limits.Image.isImage f).isoExt (FGModuleCat.imageFactorisation f).isImage

@[simp]

theorem FGModuleCat.imageIsoRange_hom_comp {R : Type u} [CommRing R] [IsNoetherianRing R] {G H : FGModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (imageIsoRange f).hom (ofHom (LinearMap.range (ModuleCat.Hom.hom f)).subtype) = CategoryTheory.Limits.image.ι f

@[simp]

theorem FGModuleCat.imageIsoRange_inv_comp {R : Type u} [CommRing R] [IsNoetherianRing R] {G H : FGModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (imageIsoRange f).inv (CategoryTheory.Limits.image.ι f) = ofHom (LinearMap.range (ModuleCat.Hom.hom f)).subtype

theorem FGModuleCat.exact_iff {R : Type u} [CommRing R] [IsNoetherianRing R] (S : CategoryTheory.ShortComplex (FGModuleCat R)) : S.Exact ↔ LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)

theorem FGModuleCat.exact_iff' {R : Type u} [CommRing R] [IsNoetherianRing R] (S : CategoryTheory.ShortComplex (FGModuleCat R)) : S.Exact ↔ Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)