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 = (LinearMap.range f).subtype

instance ModuleCat.instMonoι {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

• ModuleCat.image.lift F' = { toFun := fun (x : ↑(ModuleCat.image f)) => F'.e ↑(Classical.indefiniteDescription (fun (x_1 : ↑G) => f x_1 = ↑x) ⋯), map_add' := ⋯, map_smul' := ⋯ }

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.Image.isImage f).isoExt (ModuleCat.isImage f)

@[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.asHom (LinearMap.range f).subtype

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.asHom (LinearMap.range f).subtype) 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.of R ↥(LinearMap.range f))) : (CategoryTheory.Limits.image.ι f) ((ModuleCat.imageIsoRange f).inv x) = (ModuleCat.asHom (LinearMap.range f).subtype) 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.asHom (LinearMap.range f).subtype) = CategoryTheory.Limits.image.ι 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.asHom (LinearMap.range f).subtype) 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.asHom (LinearMap.range f).subtype) ((ModuleCat.imageIsoRange f).hom x) = (CategoryTheory.Limits.image.ι f) x