Documentation

Mathlib.Algebra.Category.ModuleCat.EpiMono

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.

Equations
Instances For
    Equations
    • =
    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
    • =