# 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 : } {H : } (f : G H) :

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

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

The inclusion of image f into the target

Equations
• = ().subtype
Instances For
instance ModuleCat.instMonoι {R : Type u} [Ring R] {G : } {H : } (f : G H) :
Equations
• =
def ModuleCat.factorThruImage {R : Type u} [Ring R] {G : } {H : } (f : G H) :

The corestriction map to the image

Equations
Instances For
theorem ModuleCat.image.fac {R : Type u} [Ring R] {G : } {H : } (f : G H) :
noncomputable def ModuleCat.image.lift {R : Type u} [Ring R] {G : } {H : } {f : G H} :
F'.I

The universal property for the image factorisation

Equations
Instances For
theorem ModuleCat.image.lift_fac {R : Type u} [Ring R] {G : } {H : } {f : G H} :
def ModuleCat.monoFactorisation {R : Type u} [Ring R] {G : } {H : } (f : G H) :

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

Equations
Instances For
noncomputable def ModuleCat.isImage {R : Type u} [Ring R] {G : } {H : } (f : G H) :

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

Equations
• = { lift := ModuleCat.image.lift, lift_fac := }
Instances For
noncomputable def ModuleCat.imageIsoRange {R : Type u} [Ring R] {G : } {H : } (f : G H) :

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

Equations
Instances For
theorem ModuleCat.imageIsoRange_inv_image_ι_assoc {R : Type u} [Ring R] {G : } {H : } (f : G H) {Z : } (h : H Z) :
theorem ModuleCat.imageIsoRange_inv_image_ι_apply {R : Type u} [Ring R] {G : } {H : } (f : G H) (x : .obj ) :
(() x) = x
@[simp]
theorem ModuleCat.imageIsoRange_inv_image_ι {R : Type u} [Ring R] {G : } {H : } (f : G H) :
theorem ModuleCat.imageIsoRange_hom_subtype_assoc {R : Type u} [Ring R] {G : } {H : } (f : G H) {Z : } (h : ModuleCat.of R H Z) :
theorem ModuleCat.imageIsoRange_hom_subtype_apply {R : Type u} [Ring R] {G : } {H : } (f : G H) (x : .obj ) :
(ModuleCat.ofHom ().subtype) (.hom x) =
@[simp]
theorem ModuleCat.imageIsoRange_hom_subtype {R : Type u} [Ring R] {G : } {H : } (f : G H) :