module Cat.Morphism.Factorisation where

# Orthogonal factorisation systemsπ

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 sets1, 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 .

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 = \operatorname{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 = \operatorname{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 = \operatorname{id}_{}$ by fitting it into a lifting diagram. But since $e \mathrel{\bot} m$, the factorisation is unique, and $gm = \operatorname{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

1. Or, more generally, in every topos.β©οΈ

2. Weβll see, in a bit, that the converse is true, too.β©οΈ