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.

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

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

Instances For