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 C\mathcal{C} and you, inspired by the wisdom of King Solomon, want to chop every morphism in half. A factorisation system (E,M)(E, M) on C\mathcal{C} will provide a tool for doing so, in a particularly coherent way. Here, EE and MM are predicates on the space of morphisms of CC. First, we package the data of an (E,M)(E, M)-factorisation of a morphism f:abf : 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 EE and MM. Generically, we call the EE-morphism in the factorisation mediate, and the MM-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:abf : a \to b factors as a map f:aer(f)mf : a {\xrightarrow{e}} r(f) {\xrightarrow{m}} where eEe \in E and mMm \in M, the classes must satisfy the following properties:

  • Every isomorphism is in both EE and in MM.2

  • Both classes are stable under composition: if fEf \in E and gEg \in E, then (gf)E(g \circ f) \in E and the same for MM

  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 EE is exactly the class of morphisms left-orthogonal to MM: A map satisfies fEf \in E if, and only if, for every gMg \in M, we have fgf {\mathrel{\bot}}g. Conversely, a map has gMg \in M if, and only if, we have fgf {\mathrel{\bot}}g for every fEf \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 ff we exhibit an isomorphism between their replacements r(f)r(f), 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=mef = m \circ e and f=mef = m' \circ e' are both (E,M)(E,M)-factorisations of ff. We use the fact that eme {\mathrel{\bot}}m' and eme' {\mathrel{\bot}}m to get maps u,vu, v satisfying um=mum = m', mu=mm'u = m, ve=eve = e', and ev=ee'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 uu and vv are inverses, fit first ee and mm into a lifting diagram like the one below. Since eme {\mathrel{\bot}}m, we have that the space of diagonals r(f)r(f)r(f) \to r(f) is contractible, hence a proposition, and since both vuvu and the identity are in that diagonal, uv=iduv = {{\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 ee' and mm' 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 EME \cap M is precisely the class of isomorphisms of ff. 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 EE is precisely M^\bot M, the class of morphisms left-orthogonal to those in MM. 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 ff is left-orthogonal to every mMm \in M, and write out the (E,M)(E,M)-factorisation f=mef = m \circ e. By a syntactic limitation in Agda, we start with the conclusion: We’ll show that mm is in EE, and since EE is closed under composition, so is ff. Since ff is orthogonal to mm, we can fit it into a lifting diagram

and make note of the diagonal filler g:Br(f)g : B \to r(f), and that it satisfies gf=egf=e and mg=idmg = {{\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=idgm = {{\mathrm{id}}_{}} by fitting it into a lifting diagram. But since eme {\mathrel{\bot}}m, the factorisation is unique, and gm=idgm = {{\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: mm is in EE, so since f=mef = m \circ e and EE is stable, so is ff!

        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.↩︎


References