open import Cat.Morphism.Factorisation
open import Cat.Morphism.Orthogonal
open import Cat.Morphism.Class
open import Cat.Morphism.Lifts
open import Cat.Prelude

import Cat.Reasoning

module Cat.Morphism.Factorisation.Orthogonal where

Orthogonal factorisation systems🔗

module _
  {o ℓ ℓl ℓr}
  (C : Precategory o ℓ)
  (L : Arrows C ℓl)
  (R : Arrows C ℓr) where
  private module C = Cat.Reasoning C
  open Factorisation

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

  record is-ofs : Type (o ⊔ ℓ ⊔ ℓl ⊔ ℓr) where
    field
      factor : ∀ {a b} (f : C.Hom a b) → Factorisation C L R f

In addition to mandating that every map $f:a\to b$ factors as a map $f:a\stackrel{l}{\to }m(f)\stackrel{r}{\to }b$ where $l\in L$ and $r\in R\text{,}$ the classes must satisfy the following properties:

• Every isomorphism is in both $L$ and in $R$¹.

• Both classes are stable under composition: if $f\in L$ and $g\in L\text{,}$ then $(g\circ f)\in L\text{,}$ and likewise for $R\text{.}$

      is-iso→in-L : ∀ {a b} (f : C.Hom a b) → C.is-invertible f → f ∈ L
      L-is-stable
        : ∀ {a b c} (f : C.Hom b c) (g : C.Hom a b) → f ∈ L → g ∈ L
        → (f C.∘ g) ∈ L

      is-iso→in-R : ∀ {a b} (f : C.Hom a b) → C.is-invertible f → f ∈ R
      R-is-stable
        : ∀ {a b c} (f : C.Hom b c) (g : C.Hom a b) → f ∈ R → g ∈ R
        → (f C.∘ g) ∈ R

Most importantly, the class $L$ is orthogonal to $R\text{,}$ i.e: for every $l\in L$ and $r\in R\text{,}$ we have $l\perp r\text{.}$²

      L⊥R : Orthogonal C L R

The canonical example of an orthogonal factorisation system is the (surjective, injective) factorisation system on the category of sets, which uniquely factors a function $f:A\to B$ through the image of $f\text{.}$³

module _
  {o ℓ ℓl ℓr}
  (C : Precategory o ℓ)
  (L : Arrows C ℓl)
  (R : Arrows C ℓr)
  (fs : is-ofs C L R)
  where

  private module C = Cat.Reasoning C
  open is-ofs fs
  open Factorisation

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 $m(f)\text{,}$ $m^{\prime }(f)$ which commutes with both the left morphism and the right 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 L R f)
    → Σ[ f ∈ fa1 .mid C.≅ fa2 .mid ]
        ( (f .C.to C.∘ fa1 .left ≡ fa2 .left)
        × (fa1 .right C.∘ f .C.from ≡ fa2 .right))
  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=r\circ l$ and $f=r^{\prime }\circ l^{\prime }$ are both $(L,R)\text{-factorisations}$ of $f\text{.}$ We use the fact that $l\perp r^{\prime }$ and $l^{\prime }\perp r$ to get maps $u,v$ satisfying $ur=r^{\prime }\text{,}$ $r^{\prime }u=r\text{,}$ $vl=l^{\prime }\text{,}$ and $l^{\prime }v=l\text{.}$

      upq =
        L⊥R _ (fa1 .left∈L) _ (fa2 .right∈R) _ _
          (sym (fa1 .factors) ∙ fa2 .factors) .centre

      vp'q' = L⊥R _ (fa2 .left∈L) _ (fa1 .right∈R) _ _
        (sym (fa2 .factors) ∙ fa1 .factors) .centre

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

      vu=id : upq .fst C.∘ vp'q' .fst ≡ C.id
      vu=id = ap fst $ is-contr→is-prop
        (L⊥R _ (fa2 .left∈L) _ (fa2 .right∈R) _ _ 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 $l^{\prime }$ and $r^{\prime }$ 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.

      uv=id : vp'q' .fst C.∘ upq .fst ≡ C.id
      uv=id = ap fst $ is-contr→is-prop
        (L⊥R _ (fa1 .left∈L) _ (fa1 .right∈R) _ _ refl)
        ( vp'q' .fst C.∘ upq .fst
        , C.pullr (upq .snd .fst) ∙ vp'q' .snd .fst
        , C.pulll (vp'q' .snd .snd) ∙ upq .snd .snd
        ) (C.id , C.idl _ , C.idr _)

  factorisation-unique
    : ∀ {a b} (f : C.Hom a b) → is-category C → is-prop (Factorisation C L R 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 .mid   = c-cat .to-path (isop1p2 .fst) i
    go i .left  = p i
    go i .right = q i

    go i .left∈L  = is-prop→pathp (λ i → is-tr (L · (p i))) (x .left∈L) (y .left∈L) i
    go i .right∈R = is-prop→pathp (λ i → is-tr (R · (q i))) (x .right∈R) (y .right∈R) i
    go i .factors =
      is-prop→pathp (λ i → C.Hom-set _ _ f (q i C.∘ p i)) (x .factors) (y .factors) i

As a passing observation, note that the intersection $L\cap R$ is precisely the class of isomorphisms of $f\text{.}$ 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 ∈ L → f ∈ R → C.is-invertible f
  in-intersection→is-iso f f∈L f∈R = self-orthogonal→invertible C f $ L⊥R f f∈L f f∈R

  in-intersection≃is-iso
    : ∀ {a b} (f : C.Hom a b) → C.is-invertible f ≃ (f ∈ L × f ∈ R)
  in-intersection≃is-iso f = prop-ext!
    (λ fi → is-iso→in-L f fi , is-iso→in-R f fi)
    λ { (a , b) → in-intersection→is-iso f a b }

The final observation is that the class $L$ is precisely ${}^{\perp }R\text{,}$ the class of morphisms left-orthogonal to those in $R\text{.}$ One direction is by definition, and the other is rather technical. Let’s focus on the technical one.

  L-is-⊥R
    : ∀ {a b} (f : C.Hom a b)
    → (f ∈ L) ≃ (∀ {c d} (m : C.Hom c d) → m ∈ R → Orthogonal C f m)
  L-is-⊥R f = prop-ext! (λ m f∈L m∈R → to f∈L m m∈R) from where
    to : ∀ {c d} (m : C.Hom c d) → f ∈ L → m ∈ R → Orthogonal C f m
    to m f∈L m∈R u v square = L⊥R f f∈L m m∈R u v square

    from : (∀ {c d} (m : C.Hom c d) → m ∈ R → Orthogonal C f m) → f ∈ L
    from ortho = subst (_∈ L) (sym (fa .factors)) $ L-is-stable _ _ m∈L (fa .left∈L)
      where

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

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

      fa = factor f
      gpq = ortho (fa .right) (fa .right∈R) (fa .left) C.id (C.idl _ ∙ (fa .factors))

We’ll show $gr=\mathrm{id}$ by fitting it into a lifting diagram. But since $l\perp r\text{,}$ the factorisation is unique, and $gr=\mathrm{id}\text{,}$ as needed.

      gm=id : gpq .centre .fst C.∘ (fa .right) ≡ C.id
      gm=id = ap fst $ is-contr→is-prop
        (L⊥R _ (fa .left∈L) _ (fa .right∈R) _ _ 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: $r$ is in $L\text{,}$ so since $f=r\circ l$ and $R$ is stable, so is $f\text{!}$

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