open import Cat.Functor.FullSubcategory
open import Cat.Morphism.Orthogonal
open import Cat.Diagram.Terminal
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 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 = {{\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


1. Or, more generally, in every topos.↩︎

2. We’ll see, in a bit, that the converse is true, too.↩︎