module Cat.Morphism.Factorisation where

Orthogonal factorisation systemsπŸ”—

Suppose you have some category and you, inspired by the wisdom of King Solomon, want to chop every morphism in half. A factorisation system on will provide a tool for doing so, in a particularly coherent way. Here, and are predicates on the space of morphisms of First, we package the data of an of a morphism

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 and Generically, we call the in the factorisation mediate, and the forget.

  record Factorisation {a b} (f : C.Hom a b) : Type (o βŠ” β„“) where
      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 factors as a map where and the classes must satisfy the following properties:

  • Every isomorphism is in both and in 2

  • Both classes are stable under composition: if and then and the same for

  record is-factorisation-system : Type (o βŠ” β„“) where
      factor : βˆ€ {a b} (f : C.Hom a b) β†’ Factorisation f

      is-isoβ†’in-E : βˆ€ {a b} (f : C.Hom a b) β†’ f β†’ f ∈ E
        : βˆ€ {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) β†’ f β†’ f ∈ M
        : βˆ€ {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 is exactly the class of morphisms left-orthogonal to A map satisfies if, and only if, for every we have Conversely, a map has if, and only if, we have for every

      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 we exhibit an isomorphism between their replacements which commutes with both the mediate morphism and the forget morphism. We reproduce the proof from (Borceux 1994, vol. 1, sec. 5.5).

    : βˆ€ {a b} (f : C.Hom a b) (fa1 fa2 : Factorisation C E M f)
    β†’ Ξ£[ f ∈ fa1 .mediating C.β‰… fa2 .mediating ]
        ( (f 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

Suppose that and are both of We use the fact that and to get maps satisfying and

      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 and are inverses, fit first and into a lifting diagram like the one below. Since we have that the space of diagonals is contractible, hence a proposition, and since both and the identity are in that diagonal,

      vu=id : upq .fst C.∘ vp'q' .fst ≑
      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.idl _ , C.idr _)

A dual argument works by making a lifting square with and 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.

    : βˆ€ {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 is precisely the class of isomorphisms of 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.

    : βˆ€ {a b} (f : C.Hom a b) β†’ f ∈ E β†’ f ∈ M β†’ f
  in-intersectionβ†’is-iso f f∈E f∈M = self-orthogonalβ†’is-iso C f $ EβŠ₯M f f f∈E f∈M

    : βˆ€ {a b} (f : C.Hom a b) β†’ f ≃ ((f ∈ E) Γ— (f ∈ M))
  in-intersection≃is-iso f = prop-ext!
    (λ 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 is precisely the class of morphisms left-orthogonal to those in One direction is by definition, and the other is rather technical. Let’s focus on the technical one.

    : βˆ€ {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
      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

Suppose that is left-orthogonal to every and write out the By a syntactic limitation in Agda, we start with the conclusion: We’ll show that is in and since is closed under composition, so is Since is orthogonal to we can fit it into a lifting diagram

and make note of the diagonal filler and that it satisfies and

        fa = factor f
        module fa = Factorisation fa
        gpq = ortho fa.forget fa.forget∈M {v =} (C.idl _ βˆ™ fa.factors)

We’ll show by fitting it into a lifting diagram. But since the factorisation is unique, and as needed.

        gm=id : gpq .centre .fst C.∘ fa.forget ≑
        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.idl _ , C.idr _)

Think back to the conclusion we wanted to reach: is in so since and is stable, so is

        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.β†©οΈŽ