open import Cat.Functor.FullSubcategory open import Cat.Morphism.Orthogonal open import Cat.Diagram.Terminal open import Cat.Functor.Adjoint open import Cat.Prelude open import Data.Power import Cat.Reasoning module Cat.Morphism.Factorisation where

Suppose you have some category
$\mathcal{C}$
and you, inspired by the wisdom of King Solomon, want to chop every
morphism in half. A **factorisation system**
$(E, M)$
on
$\mathcal{C}$
will provide a tool for doing so, in a particularly coherent way. Here,
$E$
and
$M$
are predicates on the space of morphisms of
$C$.
First, we package the data of an
$(E, M)$-factorisation
of a morphism
$f : a \to b$.

Note that while the archetype for a factorisation system is the (epi,
mono)-factorisation system on the category of sets^{1}, so
that it’s very hard *not* to refer to these things as images, it
is *not* the case, in general, nothing is required about the
interaction of epis and monos with the classes
$E$
and
$M$.
Generically, we call the
$E$-morphism
in the factorisation mediate, and the
$M$-morphism
forget.

record Factorisation {a b} (f : C.Hom a b) : Type (o ⊔ ℓ) where field mediating : C.Ob mediate : C.Hom a mediating forget : C.Hom mediating b mediate∈E : mediate ∈ E forget∈M : forget ∈ M factors : f ≡ forget C.∘ mediate

In addition to mandating that every map $f : a \to b$ factors as a map $f : a {\xrightarrow{e}} r(f) {\xrightarrow{m}}$ where $e \in E$ and $m \in M$, the classes must satisfy the following properties:

Every isomorphism is in both $E$ and in $M$.

^{2}Both classes are stable under composition: if $f \in E$ and $g \in E$, then $(g \circ f) \in E$ and the same for $M$

record is-factorisation-system : Type (o ⊔ ℓ) where field factor : ∀ {a b} (f : C.Hom a b) → Factorisation f is-iso→in-E : ∀ {a b} (f : C.Hom a b) → C.is-invertible f → f ∈ E E-is-stable : ∀ {a b c} (g : C.Hom b c) (f : C.Hom a b) → f ∈ E → g ∈ E → (g C.∘ f) ∈ E is-iso→in-M : ∀ {a b} (f : C.Hom a b) → C.is-invertible f → f ∈ M M-is-stable : ∀ {a b c} (g : C.Hom b c) (f : C.Hom a b) → f ∈ M → g ∈ M → (g C.∘ f) ∈ M

Most importantly, the class $E$ is exactly the class of morphisms left-orthogonal to $M$: A map satisfies $f \in E$ if, and only if, for every $g \in M$, we have $f {\mathrel{\bot}}g$. Conversely, a map has $g \in M$ if, and only if, we have $f {\mathrel{\bot}}g$ for every $f \in E$.

E⊥M : ∀ {a b c d} (f : C.Hom a b) (g : C.Hom c d) → f ∈ E → g ∈ M → m⊥m C f g

The first thing we observe is that factorisations for a morphism are unique. Working in precategorical generality, we weaken this to essential uniqueness: Given two factorisations of $f$ we exhibit an isomorphism between their replacements $r(f)$, $r'(f)$ which commutes with both the mediate morphism and the forget morphism. We reproduce the proof from (Borceux 1994, vol. 1, sec. 5.5).

factorisation-essentially-unique : ∀ {a b} (f : C.Hom a b) (fa1 fa2 : Factorisation C E M f) → Σ[ f ∈ fa1 .mediating C.≅ fa2 .mediating ] ( (f .C.to C.∘ fa1 .mediate ≡ fa2 .mediate) × (fa1 .forget C.∘ f .C.from ≡ fa2 .forget)) factorisation-essentially-unique f fa1 fa2 = C.make-iso (upq .fst) (vp′q′ .fst) vu=id uv=id , upq .snd .fst , vp′q′ .snd .snd where

Suppose that $f = m \circ e$ and $f = m' \circ e'$ are both $(E,M)$-factorisations of $f$. We use the fact that $e {\mathrel{\bot}}m'$ and $e' {\mathrel{\bot}}m$ to get maps $u, v$ satisfying $um = m'$, $m'u = m$, $ve = e'$, and $e'v = e$.

module fa1 = Factorisation fa1 module fa2 = Factorisation fa2 upq = E⊥M fa1.mediate fa2.forget fa1.mediate∈E fa2.forget∈M (sym fa1.factors ∙ fa2.factors) .centre vp′q′ = E⊥M fa2.mediate fa1.forget fa2.mediate∈E fa1.forget∈M (sym fa2.factors ∙ fa1.factors) .centre

To show that $u$ and $v$ are inverses, fit first $e$ and $m$ into a lifting diagram like the one below. Since $e {\mathrel{\bot}}m$, we have that the space of diagonals $r(f) \to r(f)$ is contractible, hence a proposition, and since both $vu$ and the identity are in that diagonal, $uv = {{\mathrm{id}}_{}}$.

vu=id : upq .fst C.∘ vp′q′ .fst ≡ C.id vu=id = ap fst $ is-contr→is-prop (E⊥M fa2.mediate fa2.forget fa2.mediate∈E fa2.forget∈M refl) ( upq .fst C.∘ vp′q′ .fst , C.pullr (vp′q′ .snd .fst) ∙ upq .snd .fst , C.pulll (upq .snd .snd) ∙ vp′q′ .snd .snd ) (C.id , C.idl _ , C.idr _)

A dual argument works by making a lifting square with $e'$ and $m'$ as its faces. We omit it for brevity. By the characterisation of path spaces in categories, this implies that factorisations of a fixed morphism are a proposition.

factorisation-unique : ∀ {a b} (f : C.Hom a b) → is-category C → is-prop (Factorisation C E M f) factorisation-unique f c-cat x y = go where isop1p2 = factorisation-essentially-unique f x y p = Univalent.Hom-pathp-reflr-iso c-cat {q = isop1p2 .fst} (isop1p2 .snd .fst) q = Univalent.Hom-pathp-refll-iso c-cat {p = isop1p2 .fst} (isop1p2 .snd .snd) go : x ≡ y go i .mediating = c-cat .to-path (isop1p2 .fst) i go i .mediate = p i go i .forget = q i

As a passing observation, note that the intersection $E \cap M$ is precisely the class of isomorphisms of $f$. Every isomorphism is in both classes, by the definition, and if a morphism is in both classes, it is orthogonal to itself, hence an isomorphism.

in-intersection→is-iso : ∀ {a b} (f : C.Hom a b) → f ∈ E → f ∈ M → C.is-invertible f in-intersection→is-iso f f∈E f∈M = self-orthogonal→is-iso C f $ E⊥M f f f∈E f∈M in-intersection≃is-iso : ∀ {a b} (f : C.Hom a b) → C.is-invertible f ≃ ((f ∈ E) × (f ∈ M)) in-intersection≃is-iso f = prop-ext (hlevel 1) (×-is-hlevel 1 hlevel! hlevel!) (λ fi → is-iso→in-E f fi , is-iso→in-M f fi) λ { (a , b) → in-intersection→is-iso f a b }

The final observation is that the class $E$ is precisely $^\bot M$, the class of morphisms left-orthogonal to those in $M$. One direction is by definition, and the other is rather technical. Let’s focus on the technical one.

E-is-⊥M : ∀ {a b} (f : C.Hom a b) → (f ∈ E) ≃ (∀ {c d} (m : C.Hom c d) → m ∈ M → m⊥m C f m) E-is-⊥M f = prop-ext (E f .is-tr) (hlevel 1) (λ m f∈E m∈M → to f∈E m m∈M) from where to : ∀ {c d} (m : C.Hom c d) → f ∈ E → m ∈ M → m⊥m C f m to m f∈E m∈M {u} {v} square = E⊥M f m f∈E m∈M square from : (∀ {c d} (m : C.Hom c d) → m ∈ M → m⊥m C f m) → f ∈ E from ortho = subst (_∈ E) (sym fa.factors) $ E-is-stable _ _ fa.mediate∈E m∈E where

Suppose that $f$ is left-orthogonal to every $m \in M$, and write out the $(E,M)$-factorisation $f = m \circ e$. By a syntactic limitation in Agda, we start with the conclusion: We’ll show that $m$ is in $E$, and since $E$ is closed under composition, so is $f$. Since $f$ is orthogonal to $m$, we can fit it into a lifting diagram

and make note of the diagonal filler $g : B \to r(f)$, and that it satisfies $gf=e$ and $mg = {{\mathrm{id}}_{}}$.

fa = factor f module fa = Factorisation fa gpq = ortho fa.forget fa.forget∈M {v = C.id} (C.idl _ ∙ fa.factors)

We’ll show $gm = {{\mathrm{id}}_{}}$ by fitting it into a lifting diagram. But since $e {\mathrel{\bot}}m$, the factorisation is unique, and $gm = {{\mathrm{id}}_{}}$, as needed.

gm=id : gpq .centre .fst C.∘ fa.forget ≡ C.id gm=id = ap fst $ is-contr→is-prop (E⊥M fa.mediate fa.forget fa.mediate∈E fa.forget∈M refl) ( _ , C.pullr (sym fa.factors) ∙ gpq .centre .snd .fst , C.cancell (gpq .centre .snd .snd)) (C.id , C.idl _ , C.idr _)

Think back to the conclusion we wanted to reach: $m$ is in $E$, so since $f = m \circ e$ and $E$ is stable, so is $f$!

m∈E : fa.forget ∈ E m∈E = is-iso→in-E fa.forget $ C.make-invertible (gpq .centre .fst) (gpq .centre .snd .snd) gm=id

## References

- Borceux, Francis. 1994.
*Handbook of Categorical Algebra*. Vol. 1. Encyclopedia of Mathematics and Its Applications. Cambridge University Press. https://doi.org/10.1017/CBO9780511525858.