open import Cat.Functor.Adjoint.Reflective
open import Cat.Functor.WideSubcategory
open import Cat.Morphism.Factorisation
open import Cat.Morphism.Orthogonal
open import Cat.Functor.Adjoint
open import Cat.Morphism.Class
open import Cat.Morphism.Lifts
open import Cat.Prelude

import Cat.Functor.Reasoning.FullyFaithful
import Cat.Functor.Reasoning
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 $C$ and you, inspired by the wisdom of King Solomon, want to chop every morphism in half. An orthogonal factorisation system $(L, R)$ on $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 .$ First, we package the data of an $(L, R)$ -factorisation of a morphism $f : a \to b .$

  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 l m (f) r b$ where $l \in L$ and $r \in R,$ 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,$ then $(g \circ f) \in L,$ and likewise for $R .$

      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,$ i.e: for every $l \in L$ and $r \in R,$ we have $l ⊥ r .$ ²

      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 .$ ³

    L-subcat : Wide-subcat C ℓl
    L-subcat .Wide-subcat.P f = f ∈ L
    L-subcat .Wide-subcat.P-prop f = hlevel 1
    L-subcat .Wide-subcat.P-id = is-iso→in-L C.id C.id-invertible
    L-subcat .Wide-subcat.P-∘ = L-is-stable _ _

    R-subcat : Wide-subcat C ℓr
    R-subcat .Wide-subcat.P f = f ∈ R
    R-subcat .Wide-subcat.P-prop f = hlevel 1
    R-subcat .Wide-subcat.P-id = is-iso→in-R C.id C.id-invertible
    R-subcat .Wide-subcat.P-∘ = R-is-stable _ _

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),$ $m^{'} (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^{'} \circ l^{'}$ are both $(L, R) -factorisations$ of $f .$ We use the fact that $l ⊥ r^{'}$ and $l^{'} ⊥ r$ to get maps $u, v$ satisfying $u r = r^{'},$ $r^{'} u = r,$ $v l = l^{'},$ and $l^{'} v = l .$

      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 ⊥ r,$ 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 = id .$

      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^{'}$ and $r^{'}$ 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 .$ 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 $^{⊥} R,$ the class of morphisms left-orthogonal to those in $R .$ 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,$ and write out the $(L, R) -factorisation$ $f = r \circ l .$ By a syntactic limitation in Agda, we start with the conclusion: We’ll show that $r$ is in $L,$ and since $L$ is closed under composition, so is $f .$ Since $f$ is orthogonal to $r,$ we can fit it into a lifting diagram

and make note of the diagonal filler $g : B \to r (f),$ and that it satisfies $g f = e$ and $m g = id .$

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

We’ll show $g r = id$ by fitting it into a lifting diagram. But since $l ⊥ r,$ the factorisation is unique, and $g r = id,$ 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,$ so since $f = r \circ l$ and $R$ is stable, so is $f!$

      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

Reflecting orthogonal factorisations systems🔗

Let $D$ be a category equipped with an orthogonal factorisation system $(L, R),$ and $ι : C \to D$ be a reflective subcategory of $D$ with reflector $r ⊣ ι .$ If $L \subseteq (ι \circ r)^{*} L$ and $R \subseteq (ι \circ r)^{*} R,$ then $(ι^{*} L, ι^{*} R)$ forms an orthogonal factorisation system on $C .$

module _
  {oc ℓc od ℓd ℓld ℓrd}
  {C : Precategory oc ℓc} {D : Precategory od ℓd}
  {L : Arrows D ℓld} {R : Arrows D ℓrd}
  {ι : Functor C D} {r : Functor D C}
  where

  reflect-ofs
    : (r⊣ι : r ⊣ ι)
    → is-reflective r⊣ι
    → L ⊆ F-restrict-arrows (ι F∘ r) L
    → R ⊆ F-restrict-arrows (ι F∘ r) R
    → is-ofs D L R
    → is-ofs C (F-restrict-arrows ι L) (F-restrict-arrows ι R)
  reflect-ofs r⊣ι ι-ff ι∘r-in-L ι∘r-in-R D-ofs = C-ofs where

    module C = Cat.Reasoning C
    module D where
      open Cat.Reasoning D public
      open is-ofs D-ofs public

    module ι = Cat.Functor.Reasoning.FullyFaithful ι ι-ff
    module r = Cat.Functor.Reasoning r
    open _⊣_ r⊣ι

    open is-ofs
    open Factorisation

First, some preliminaries. Note that $ι^{*} (L)$ is closed under composition and inverses, as $ι$ preserves isomorphisms and is functorial.

    is-iso→in-ι^*L
      : ∀ {a b}
      → (f : C.Hom a b)
      → C.is-invertible f
      → ι.₁ f ∈ L
    is-iso→in-ι^*L f f-inv = D.is-iso→in-L (ι.F₁ f) (ι.F-map-invertible f-inv)

    ι^*L-is-stable
      : ∀ {a b c}
      → (f : C.Hom b c) (g : C.Hom a b)
      → ι.₁ f ∈ L → ι.₁ g ∈ L
      → ι.₁ (f C.∘ g) ∈ L
    ι^*L-is-stable f g ι[f]∈L ι[g]∈L =
      subst (_∈ L) (sym (ι.F-∘ f g)) $
      D.L-is-stable (ι.F₁ f) (ι.F₁ g) ι[f]∈L ι[g]∈L

A similar argument lets us conclude that $ι^{*} (R)$ is also closed under composition and inverses.

    is-iso→in-ι^*R
      : ∀ {a b}
      → (f : C.Hom a b)
      → C.is-invertible f
      → ι.₁ f ∈ R
    is-iso→in-ι^*R f f-inv = D.is-iso→in-R (ι.F₁ f) (ι.F-map-invertible f-inv)

    ι^*R-is-stable
      : ∀ {a b c}
      → (f : C.Hom b c) (g : C.Hom a b)
      → ι.₁ f ∈ R → ι.₁ g ∈ R
      → ι.₁ (f C.∘ g) ∈ R
    ι^*R-is-stable f g ι[f]∈R ι[g]∈R =
      subst (_∈ R) (sym (ι.F-∘ f g)) $
      D.R-is-stable (ι.F₁ f) (ι.F₁ g) ι[f]∈R ι[g]∈R

Next, recall that if $r ⊣ ι$ is reflective, then the counit of the adjunction must be invertible.

    ε-inv : ∀ (x : C.Ob) → C.is-invertible (ε x)
    ε-inv x = is-reflective→counit-is-invertible r⊣ι ι-ff

    module ε (x : C.Ob) = C.is-invertible (ε-inv x)

With those preliminaries out of the way, we can get into the meat of the proof. We’ve already proved the requisite closure properties of $ι^{*} (L)$ and $ι^{*} (R),$ so we can get that out of the way.

    C-ofs : is-ofs C (F-restrict-arrows ι L) (F-restrict-arrows ι R)
    C-ofs .is-iso→in-L = is-iso→in-ι^*L
    C-ofs .L-is-stable = ι^*L-is-stable
    C-ofs .is-iso→in-R = is-iso→in-ι^*R
    C-ofs .R-is-stable = ι^*R-is-stable

Moreover, $ι^{*} (L)$ and $ι^{*} (R)$ are orthogonal, as fully faithful functors reflect orthogonality.

    C-ofs .L⊥R f ι[f]∈L g ι[g]∈R =
      ff→reflect-orthogonal ι ι-ff (D.L⊥R (ι.₁ f) ι[f]∈L (ι.₁ g) ι[g]∈R)

The final step is the most difficult. Let $f : C (a, b)$ be a morphism in $C :$ we somehow need to factor it into a $u : C (a, x)$ and $v : C (x, b)$ with $ι (u) \in L$ and $ι (v) \in R .$

We start by factoring $ι (f)$ into a $u : D (ι (a), x)$ and $v : D (x, ι (b)) .$ We can take an adjoint transpose of $u$ to find a map $C (r (x), b),$ but this same trick does not work for $u .$ Luckily the counit $ε : C (r (ι (x)), x)$ is invertible, so we can transpose $u$ to a map in $C$ via $r (u) \circ ε^{- 1} : C (a, r (x)) .$

    C-ofs .factor {a} {b} f = f-factor
      where
        module ι[f] = Factorisation (D.factor (ι.₁ f))

        f-factor : Factorisation C (F-restrict-arrows ι L) (F-restrict-arrows ι R) f
        f-factor .mid = r.₀ ι[f].mid
        f-factor .left = r.₁ ι[f].left C.∘ ε.inv a
        f-factor .right = ε b C.∘ r.₁ ι[f].right

A bit of quick algebra shows that these two transposes actually factor $f .$

        f-factor .factors =
          f                                                        ≡⟨ C.intror (ε.invl a) ⟩
          f C.∘ ε _ C.∘ ε.inv a                                    ≡⟨ C.extendl (sym $ counit.is-natural a b f) ⟩
          ε b C.∘ r.F₁ (ι.₁ f) C.∘ ε.inv a                         ≡⟨ C.push-inner (r.expand ι[f].factors) ⟩
          (ε b C.∘ r.₁ ι[f].right) C.∘ (r.₁ ι[f].left C.∘ ε.inv a) ∎

Finally, we need to show that $ι (r (u) \circ ε^{- 1}) \in L$ and $ι (ε \circ r (v)) \in R .$ Both $ι (L)$ and $ι (R)$ are closed under inverses and composition, so it suffices to show that $ι (r (u)) \in L$ and $ι (r (v)) \in R .$ By assumption, we have $L \subseteq (ι \circ r)^{*} (L)$ and $R \subseteq (ι \circ r)^{*} (R),$ so it suffices to show that $u \in L$ and $v \in R .$ This follows from the construction of $u$ and $v$ via an $(L, R)$ factorisation, which completes the proof.

        f-factor .left∈L =
          ι^*L-is-stable (r.₁ ι[f].left) (ε.inv a)
            (ι∘r-in-L ι[f].left ι[f].left∈L)
            (is-iso→in-ι^*L (ε.inv a) (ε.op a))
        f-factor .right∈R =
          ι^*R-is-stable (ε b) (r.₁ ι[f].right)
            (is-iso→in-ι^*R (ε b) (ε-inv b))
            (ι∘r-in-R ι[f].right ι[f].right∈R)

We’ll see, in a bit, that the converse is true, too.↩︎
As we shall shortly see, $L$ is actually exactly the class of morphisms that is left orthogonal to $R$ and vice-versa for $R .$ ↩︎
This factorisation system is a special case of the (strong epimorphism, monomorphism) orthogonal factorisation system on a regular category.↩︎

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.