The category of R-modules has images.

Note that we don't need to register any of the constructions here as instances, because we get them from the fact that ModuleCat R is an abelian category.

def ModuleCat.image {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : ModuleCat R

The image of a morphism in ModuleCat R is just the bundling of LinearMap.range f

Equations

• ModuleCat.image f = ModuleCat.of R ↥(LinearMap.range f)

def ModuleCat.image.ι {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : ModuleCat.image f ⟶ H

The inclusion of image f into the target

Equations

• ModuleCat.image.ι f = Submodule.subtype (LinearMap.range f)

instance ModuleCat.instMonoModuleCatModuleCategoryImageι {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Mono (ModuleCat.image.ι f)

Equations

• ⋯ = ⋯

def ModuleCat.factorThruImage {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : G ⟶ ModuleCat.image f

The corestriction map to the image

Equations

• ModuleCat.factorThruImage f = LinearMap.rangeRestrict f

theorem ModuleCat.image.fac {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (ModuleCat.factorThruImage f) (ModuleCat.image.ι f) = f

noncomputable def ModuleCat.image.lift {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : ModuleCat.image f ⟶ F'.I

The universal property for the image factorisation

Equations

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

theorem ModuleCat.image.lift_fac {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (ModuleCat.image.lift F') F'.m = ModuleCat.image.ι f

def ModuleCat.monoFactorisation {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.MonoFactorisation f

The factorisation of any morphism in ModuleCat R through a mono.

Equations

• ModuleCat.monoFactorisation f = CategoryTheory.Limits.MonoFactorisation.mk (ModuleCat.image f) (ModuleCat.image.ι f) (ModuleCat.factorThruImage f) ⋯

noncomputable def ModuleCat.isImage {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.IsImage (ModuleCat.monoFactorisation f)

The factorisation of any morphism in ModuleCat R through a mono has the universal property of the image.

Equations

• ModuleCat.isImage f = { lift := ModuleCat.image.lift, lift_fac := ⋯ }

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

The categorical image of a morphism in ModuleCat R agrees with the linear algebraic range.

Equations

• ModuleCat.imageIsoRange f = CategoryTheory.Limits.IsImage.isoExt (CategoryTheory.Limits.Image.isImage f) (ModuleCat.isImage f)

theorem ModuleCat.imageIsoRange_inv_image_ι_assoc {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.subtype (LinearMap.range f))) h

theorem ModuleCat.imageIsoRange_inv_image_ι_apply {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.monoFactorisation f).I) : (CategoryTheory.Limits.image.ι f) (((ModuleCat.isImage f).lift (CategoryTheory.Limits.Image.monoFactorisation f)) x) = (ModuleCat.monoFactorisation f).m x

@[simp]

theorem ModuleCat.imageIsoRange_inv_image_ι {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv (CategoryTheory.Limits.image.ι f) = ModuleCat.ofHom (Submodule.subtype (LinearMap.range f))

theorem ModuleCat.imageIsoRange_hom_subtype_assoc {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : ModuleCat.of R ↑H ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.subtype (LinearMap.range f))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h

theorem ModuleCat.imageIsoRange_hom_subtype_apply {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) (x : (CategoryTheory.forget (ModuleCat R)).obj (CategoryTheory.Limits.image f)) : (ModuleCat.ofHom (Submodule.subtype (LinearMap.range f))) ((ModuleCat.imageIsoRange f).hom x) = (CategoryTheory.Limits.image.ι f) x

@[simp]

theorem ModuleCat.imageIsoRange_hom_subtype {R : Type u} [Ring R] {G : ModuleCat R} {H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).hom (ModuleCat.ofHom (Submodule.subtype (LinearMap.range f))) = CategoryTheory.Limits.image.ι f