# mathlibdocumentation

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)  :
theorem Module.range_eq_top_of_epi {R : Type u} [ring R] {X Y : Module R} (f : X Y)  :
theorem Module.mono_iff_ker_eq_bot {R : Type u} [ring R] {X Y : Module R} (f : X Y) :
theorem Module.mono_iff_injective {R : Type u} [ring R] {X Y : Module R} (f : X Y) :
theorem Module.epi_iff_range_eq_top {R : Type u} [ring R] {X Y : Module R} (f : X Y) :
theorem Module.epi_iff_surjective {R : Type u} [ring R] {X Y : Module R} (f : X Y) :
def Module.unique_of_epi_zero {R : Type u} [ring R] {M : Type v} [ M] (X : Module R) [h : category_theory.epi 0] :

If the zero morphism is an epi then the codomain is trivial.

Equations
@[protected, instance]
def Module.mono_as_hom'_subtype {R : Type u} [ring R] {X : Module R} (U : X) :
@[protected, instance]
def Module.epi_as_hom''_mkq {R : Type u} [ring R] {X : Module R} (U : X) :
@[protected, instance]
def Module.forget_preserves_epimorphisms {R : Type u} [ring R] :
@[protected, instance]