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.

theorem Subtype.ext_val_iff {α : Sort u_1} {p : α → Prop} {a1 a2 : { x : α // p x }} : a1 = a2 ↔ ↑a1 = ↑a2

def ModuleCat.image {R : Type u} [Ring R] {G 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 (ModuleCat.Hom.hom f))

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

The inclusion of image f into the target

Equations

• ModuleCat.image.ι f = ModuleCat.ofHom (LinearMap.range (ModuleCat.Hom.hom f)).subtype

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

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

The corestriction map to the image

Equations

• ModuleCat.factorThruImage f = ModuleCat.ofHom (ModuleCat.Hom.hom f).rangeRestrict

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

noncomputable def ModuleCat.image.lift {R : Type u} [Ring R] {G H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : 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 H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (lift F') F'.m = ι f

def ModuleCat.monoFactorisation {R : Type u} [Ring R] {G 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 = { I := ModuleCat.image f, m := ModuleCat.image.ι f, m_mono := ⋯, e := ModuleCat.factorThruImage f, fac := ⋯ }

noncomputable def ModuleCat.isImage {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.IsImage (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 H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.image f ≅ of R ↥(LinearMap.range (Hom.hom 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 H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (imageIsoRange f).inv (CategoryTheory.Limits.image.ι f) = ofHom (LinearMap.range (Hom.hom f)).subtype

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

theorem ModuleCat.imageIsoRange_inv_image_ι_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (of R ↥(LinearMap.range (Hom.hom f)))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) ((CategoryTheory.ConcreteCategory.hom (imageIsoRange f).inv) x) = ↑x

@[simp]

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

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

theorem ModuleCat.imageIsoRange_hom_subtype_apply {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : CategoryTheory.ToType (CategoryTheory.Limits.image f)) : ↑((CategoryTheory.ConcreteCategory.hom (imageIsoRange f).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) x