mathlib documentation

algebra.category.Module.epi_mono

Monomorphisms in `Module R` #

This file shows that an R-linear map is a monomorphism in the category of R-modules if and only if it is injective, and similarly an epimorphism if and only if it is surjective.

theorem Module.ker_eq_bot_of_mono {R : Type u} [ring R] {X Y : Module R} (f : X ⟶ Y) [category_theory.mono f] :

linear_map.ker f = ⊥

theorem Module.range_eq_top_of_epi {R : Type u} [ring R] {X Y : Module R} (f : X ⟶ Y) [category_theory.epi f] :

linear_map.range f = ⊤

theorem Module.mono_iff_ker_eq_bot {R : Type u} [ring R] {X Y : Module R} (f : X ⟶ Y) :

category_theory.mono f ↔ linear_map.ker f = ⊥

theorem Module.mono_iff_injective {R : Type u} [ring R] {X Y : Module R} (f : X ⟶ Y) :

category_theory.mono f ↔ function.injective ⇑f

theorem Module.epi_iff_range_eq_top {R : Type u} [ring R] {X Y : Module R} (f : X ⟶ Y) :

category_theory.epi f ↔ linear_map.range f = ⊤

theorem Module.epi_iff_surjective {R : Type u} [ring R] {X Y : Module R} (f : X ⟶ Y) :

category_theory.epi f ↔ function.surjective ⇑f

@[protected, instance]

def Module.mono_as_hom'_subtype {R : Type u} [ring R] {X : Module R} (U : submodule R ↥X) :

category_theory.mono ↾(U.subtype)

@[protected, instance]

def Module.epi_as_hom''_mkq {R : Type u} [ring R] {X : Module R} (U : submodule R ↥X) :

category_theory.epi ↿(U.mkq)