The category of R-modules has images. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Note that we don't need to register any of the constructions here as instances, because we get them
from the fact that Module R is an abelian category.
The image of a morphism in Module R is just the bundling of linear_map.range f
Equations
- Module.image f = Module.of R ↥(linear_map.range f)
The inclusion of image f into the target
Equations
Instances for Module.image.ι
@[protected, instance]
def
Module.factor_thru_image
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H) :
G ⟶ Module.image f
The corestriction map to the image
Equations
noncomputable
def
Module.image.lift
{R : Type u}
[comm_ring R]
{G H : Module R}
{f : G ⟶ H}
(F' : category_theory.limits.mono_factorisation f) :
Module.image f ⟶ F'.I
The universal property for the image factorisation
theorem
Module.image.lift_fac
{R : Type u}
[comm_ring R]
{G H : Module R}
{f : G ⟶ H}
(F' : category_theory.limits.mono_factorisation f) :
Module.image.lift F' ≫ F'.m = Module.image.ι f
The factorisation of any morphism in Module R through a mono.
Equations
- Module.mono_factorisation f = {I := Module.image f, m := Module.image.ι f, m_mono := _, e := Module.factor_thru_image f, fac' := _}
The factorisation of any morphism in Module R through a mono has the universal property of
the image.
Equations
- Module.is_image f = {lift := Module.image.lift f, lift_fac' := _}
@[simp]
theorem
Module.image_iso_range_inv_image_ι
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H) :
@[simp]
theorem
Module.image_iso_range_inv_image_ι_apply
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H)
(x : ↥(Module.of R ↥(linear_map.range f))) :
⇑(category_theory.limits.image.ι f) (⇑((Module.image_iso_range f).inv) x) = ⇑(Module.of_hom (linear_map.range f).subtype) x
@[simp]
theorem
Module.image_iso_range_inv_image_ι_assoc
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H)
{X' : Module R}
(f' : H ⟶ X') :
(Module.image_iso_range f).inv ≫ category_theory.limits.image.ι f ≫ f' = Module.of_hom (linear_map.range f).subtype ≫ f'
@[simp]
theorem
Module.image_iso_range_hom_subtype
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H) :
@[simp]
theorem
Module.image_iso_range_hom_subtype_assoc
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H)
{X' : Module R}
(f' : Module.of R ↥H ⟶ X') :
(Module.image_iso_range f).hom ≫ Module.of_hom (linear_map.range f).subtype ≫ f' = category_theory.limits.image.ι f ≫ f'
@[simp]
theorem
Module.image_iso_range_hom_subtype_apply
{R : Type u}
[comm_ring R]
{G H : Module R}
(f : G ⟶ H)
(x : ↥(category_theory.limits.image f)) :
⇑(Module.of_hom (linear_map.range f).subtype) (⇑((Module.image_iso_range f).hom) x) = ⇑(category_theory.limits.image.ι f) x