Epi-Mono Factorization

theorem definition

In $\mathbf{Set}$ (and in any Topos or regular category) every morphism $f:A\to B$ factors as an Epimorphism followed by a Monomorphism:

$$A\twoheadrightarrow \mathrm{im}(f)\hookrightarrow B,\mathrm{im}(f):=\{f(a)\mid a\in A\},$$

and this factorization is unique up to unique isomorphism. The image $\mathrm{im}(f)$ is a Subobject of $B$ and a quotient of $A$.

Sources: 7 Sketches §1.4.2 (pulling back partitions “by taking the epi-mono factorization”); Kittenlab Lecture 14 (direct image); DaoFP §2.4–2.5.

Uses: the right adjoint $g^{\ast }$ in Pushforward and Pullback of Partitions composes a surjection with $g$ and takes the epi part; the direct image $f_{!}(A^{\prime })$ is the image of the restriction of $f$ to $A^{\prime }$; in a Topos the image gives the existential quantifier ${\exists }_f$ (Quantification).

JuliaLeanHaskell

Docs: FinSets · C-set morphisms — Kittenlab Lecture 14

using Catlab
f = FinFunction([2, 2, 3], 4)
e, m = epi_mono(f)          # e: FinSet(3) ↠ FinSet(2), m: FinSet(2) ↪ FinSet(4)
compose(e, m) == f          # true

#check CategoryTheory.Limits.image        -- image f, with `factorThruImage f` (epi in nice categories) and `image.ι` (mono)
#check CategoryTheory.StrongEpiMonoFactorisation

import Data.List (nub)
-- image of a function on a finite domain, and the epi/mono parts
epiMono :: Eq b => [a] -> (a -> b) -> ([b], a -> Int, Int -> b)
epiMono as f = (img, \a -> length (takeWhile (/= f a) img), (img !!))
  where img = nub (map f as)