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 : ModuleCat R} {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 : ModuleCat R} {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 : ModuleCat R} {Y : ModuleCat R} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ LinearMap.ker f = ⊥

theorem ModuleCat.mono_iff_injective {R : Type u} [Ring R] {X : ModuleCat R} {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 : ModuleCat R} {Y : ModuleCat R} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ LinearMap.range f = ⊤

theorem ModuleCat.epi_iff_surjective {R : Type u} [Ring R] {X : ModuleCat R} {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

• ModuleCat.uniqueOfEpiZero X = uniqueOfSurjectiveZero ↑X (_ : Function.Surjective ⇑0)

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

Equations

• (_ : CategoryTheory.Mono (ModuleCat.asHomRight (Submodule.subtype U))) = (_ : CategoryTheory.Mono (ModuleCat.asHomRight (Submodule.subtype U)))

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

Equations

• (_ : CategoryTheory.Epi (ModuleCat.asHomLeft (Submodule.mkQ U))) = (_ : CategoryTheory.Epi (ModuleCat.asHomLeft (Submodule.mkQ U)))

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

Equations

• (_ : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget (ModuleCat R))) = (_ : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget (ModuleCat R)))

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

Equations

• (_ : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget (ModuleCat R))) = (_ : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget (ModuleCat R)))