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 ModuleCat.ker_eq_bot_of_mono {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) [CategoryTheory.Mono f] : (Hom.hom f).ker = ⊥

theorem ModuleCat.range_eq_top_of_epi {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) [CategoryTheory.Epi f] : (Hom.hom f).range = ⊤

theorem ModuleCat.mono_iff_ker_eq_bot {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ (Hom.hom f).ker = ⊥

theorem ModuleCat.mono_iff_injective {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem ModuleCat.epi_iff_range_eq_top {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ (Hom.hom f).range = ⊤

theorem ModuleCat.epi_iff_surjective {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

@[instance_reducible]

def ModuleCat.uniqueOfEpiZero {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (X : ModuleCat R) [h : CategoryTheory.Epi 0] : Unique M

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

Equations

• X.uniqueOfEpiZero = uniqueOfSurjectiveZero ↑X ⋯

instance ModuleCat.mono_as_hom'_subtype {R : Type u} [Ring R] {X : ModuleCat R} (U : Submodule R ↑X) : CategoryTheory.Mono (ofHom U.subtype)

instance ModuleCat.epi_as_hom''_mkQ {R : Type u} [Ring R] {X : ModuleCat R} (U : Submodule R ↑X) : CategoryTheory.Epi (ofHom U.mkQ)

instance ModuleCat.forget_preservesEpimorphisms {R : Type u} [Ring R] : (CategoryTheory.forget (ModuleCat R)).PreservesEpimorphisms

instance ModuleCat.forget_preservesMonomorphisms {R : Type u} [Ring R] : (CategoryTheory.forget (ModuleCat R)).PreservesMonomorphisms