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] : LinearMap.ker f = ⊥

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

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

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

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

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

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 (ModuleCat.asHomRight U.subtype)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯