open import Cat.Morphism.Class
open import Cat.Prelude

import Cat.Reasoning

module Cat.Morphism.Factorisation where

Factorisations🔗

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

Let $L, R \subseteq C$ be two classes of morphisms of $C .$ An $(L, R)$ factorisation of a morphism $f : C (X, Y)$ consists of an object $m (f) : C$ and a pair of morphisms $l : C (X, m (f)), r : C (m (f), Y)$ such that $l \in L,$ $r \in R,$ and $f = r \circ l .$

  record Factorisation {a b} (f : C.Hom a b) : Type (o ⊔ ℓ ⊔ ℓl ⊔ ℓr) where
    constructor factorisation
    field
      mid     : C.Ob
      left    : C.Hom a mid
      right   : C.Hom mid b
      left∈L  : left ∈ L
      right∈R : right ∈ R
      factors : f ≡ right C.∘ left

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

Properties of factorisations🔗

If $f$ is monic and factors as $f = r \circ l,$ then $l$ must also be monic.

  factor-monic→left-monic
    : ∀ {x y} {f : C.Hom x y}
    → (f-fac : Factorisation C L R f)
    → C.is-monic f
    → C.is-monic (f-fac .left)
  factor-monic→left-monic {f = f} f-fac f-monic = C.monic-cancell $
    C.subst-is-monic (f-fac .factors) f-monic

If $f$ is epic and factors as $f = r \circ l,$ then $r$ must also be epic.

  factor-epic→right-epic
    : ∀ {x y} {f : C.Hom x y}
    → (f-fac : Factorisation C L R f)
    → C.is-epic f
    → C.is-epic (f-fac .right)
  factor-epic→right-epic {f = f} f-fac f-epic = C.epic-cancelr $
    C.subst-is-epic (f-fac .factors) f-epic