The category of left R-modules is abelian.
Additionally, two linear maps are exact in the categorical sense iff range f = ker g.
def
Module.normal_mono
{R : Type u}
[ring R]
{M N : Module R}
(f : M ⟶ N)
(hf : category_theory.mono f) :
In the category of modules, every monomorphism is normal.
Equations
- Module.normal_mono f hf = {Z := Module.of R (linear_map.range f).quotient (submodule.quotient.semimodule (linear_map.range f)), g := (linear_map.range f).mkq, w := _, is_limit := category_theory.limits.is_kernel.iso_kernel (linear_map.range f).mkq f (Module.kernel_is_limit (linear_map.range f).mkq) (((linear_map.ker f).quot_equiv_of_eq_bot _).symm.trans ((linear_map.quot_ker_equiv_range f).trans (linear_equiv.of_eq (linear_map.range f) (linear_map.range f).mkq.ker _))).to_Module_iso' _}
def
Module.normal_epi
{R : Type u}
[ring R]
{M N : Module R}
(f : M ⟶ N)
(hf : category_theory.epi f) :
In the category of modules, every epimorphism is normal.
Equations
- Module.normal_epi f hf = {W := Module.of R ↥(linear_map.ker f) (linear_map.ker f).semimodule, g := (linear_map.ker f).subtype, w := _, is_colimit := category_theory.limits.is_cokernel.cokernel_iso (linear_map.ker f).subtype f (Module.cokernel_is_colimit (linear_map.ker f).subtype) ((((linear_map.ker f).subtype.range.quot_equiv_of_eq (linear_map.ker f) _).trans (linear_map.quot_ker_equiv_range f)).trans (linear_equiv.of_top (linear_map.range f) _)).to_Module_iso' _}
@[instance]
The category of R-modules is abelian.
Equations
- Module.category_theory.abelian = {to_preadditive := {hom_group := λ (P Q : Module R), linear_map.add_comm_group, add_comp' := _, comp_add' := _}, has_finite_products := _, has_kernels := _, has_cokernels := _, normal_mono := λ (X Y : Module R), Module.normal_mono, normal_epi := λ (X Y : Module R), Module.normal_epi}