Documentation

Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Epi and mono in concrete categories #

In this file, we relate epimorphisms and monomorphisms in a concrete category C to surjective and injective morphisms, and we show that if C has strong epi mono factorizations and is such that forget C preserves both epi and mono, then any morphism in C can be factored in a functorial manner as a composition of a surjective morphism followed by an injective morphism.

In any concrete category, injective morphisms are monomorphisms.

In any concrete category, surjective morphisms are epimorphisms.

If the forgetful functor of a concrete category reflects isomorphisms, being an isomorphism is equivalent to being bijective.