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.
The image of a morphism in ModuleCat R
is just the bundling of LinearMap.range f
Instances For
The inclusion of image f
into the target
Instances For
The corestriction map to the image
Instances For
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))))
:
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))
: