mathlib3 documentation

algebra.category.Module.abelian

The category of left R-modules is abelian. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Additionally, two linear maps are exact in the categorical sense iff range f = ker g.

noncomputable def Module.normal_mono {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) (hf : category_theory.mono f) :

category_theory.normal_mono f

In the category of modules, every monomorphism is normal.

Equations

Module.normal_mono f hf = {Z := Module.of R (↥N ⧸ linear_map.range f) {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul (submodule.quotient.has_smul' (linear_map.range f))}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}, 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.ker (linear_map.range f).mkq) _))).to_Module_iso' _}

noncomputable def Module.normal_epi {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) (hf : category_theory.epi f) :

category_theory.normal_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).module, 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.range (linear_map.ker f).subtype).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' _}

@[protected, instance]

noncomputable def Module.abelian {R : Type u} [ring R] :

category_theory.abelian (Module R)

The category of R-modules is abelian.

Equations

Module.abelian = category_theory.abelian.mk

@[protected, instance]

noncomputable def Module.forget_reflects_limits_of_size {R : Type u} [ring R] :

category_theory.limits.reflects_limits_of_size (category_theory.forget (Module R))

Equations

Module.forget_reflects_limits_of_size = category_theory.limits.reflects_limits_of_reflects_isomorphisms

@[protected, instance]

noncomputable def Module.forget₂_reflects_limits_of_size {R : Type u} [ring R] :

category_theory.limits.reflects_limits_of_size (category_theory.forget₂ (Module R) AddCommGroup)

Equations

Module.forget₂_reflects_limits_of_size = category_theory.limits.reflects_limits_of_reflects_isomorphisms

@[protected, instance]

noncomputable def Module.forget_reflects_limits {R : Type u} [ring R] :

category_theory.limits.reflects_limits (category_theory.forget (Module R))

Equations

Module.forget_reflects_limits = Module.forget_reflects_limits_of_size

@[protected, instance]

noncomputable def Module.forget₂_reflects_limits {R : Type u} [ring R] :

category_theory.limits.reflects_limits (category_theory.forget₂ (Module R) AddCommGroup)

Equations

Module.forget₂_reflects_limits = Module.forget₂_reflects_limits_of_size

theorem Module.exact_iff {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) {O : Module R} (g : N ⟶ O) :

category_theory.exact f g ↔ linear_map.range f = linear_map.ker g