The category of left R-modules is abelian.
Additionally, two linear maps are exact in the categorical sense iff range f = ker g.
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' _}
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 := id (λ (J : Type u) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape_of_has_limits), has_kernels := category_theory.limits.has_kernels_of_has_equalizers (Module R) category_theory.limits.has_limits_of_shape_of_has_limits, has_cokernels := Module.has_cokernels_Module _inst_1, normal_mono := λ (X Y : Module R), Module.normal_mono, normal_epi := λ (X Y : Module R), Module.normal_epi}