module Cat.Diagram.Colimit.Finite where

Finitely cocomplete categoriesπŸ”—

Finitely cocomplete categories are dual to finitely complete categories in that they admit colimits for all diagrams of finite shape.

  is-finitely-cocomplete : Typeω
  is-finitely-cocomplete = βˆ€ {o β„“} {D : Precategory o β„“} β†’ is-finite-precategory D
                         β†’ (F : Functor D C) β†’ Colimit F

Equivalently, a finitely cocomplete category has:

  • An initial object (colimit over the empty diagram)
  • All binary coproducts (colimits over any diagrams of shape
  • All binary coequalisers (colimits over any diagrams of shape
  • All binary pushouts (colimits over any diagrams of shape
  record Finitely-cocomplete : Type (β„“ βŠ” β„“') where
    field
      initial      : Initial C
      coproducts   : βˆ€ A B β†’ Coproduct C A B
      coequalisers : βˆ€ {A B} (f g : Hom A B) β†’ Coequaliser C f g
      pushouts     : βˆ€ {A B X} (f : Hom X A) (g : Hom X B) β†’ Pushout C f g

    Coequ : βˆ€ {A B} (f g : Hom A B) β†’ Ob
    Coequ f g = coequalisers f g .Coequaliser.coapex

    Po : βˆ€ {A B C} (f : Hom C A) (g : Hom C B) β†’ Ob
    Po f g = pushouts f g .Pushout.coapex

  open Finitely-cocomplete

As seen on the page for finitely complete categories, this definition equivalently states that a finitely cocomplete category has either of the following:

  • An initial object, all binary coproducts, and all binary coequalisers
  • An initial object and all binary pushouts

This follows from the fact that we can build coproducts and coequalisers from pushouts, and that conversely, we can build pushouts from coproducts and coequalisers. We begin by proving the latter.

With coequalisersπŸ”—

We construct a pushout under a span as a quotient object of a coproduct i.e.Β the coequaliser of and where and are injections into the coproduct.

Where is some object which admits injections and from X and Y respectively. This coequaliser represents a pushout

where is the pushout’s coapex, or equivalently, the coequaliser of and

  coproduct-coequaliser→pushout
    : βˆ€ {E P X Y Z} {in1 : Hom X P} {in2 : Hom Y P} {f : Hom Z X}
        {g : Hom Z Y} {e : Hom P E}
    β†’ is-coproduct C in1 in2
    β†’ is-coequaliser C (in1 ∘ f) (in2 ∘ g) e
    β†’ is-pushout C f (e ∘ in1) g (e ∘ in2)
  coproduct-coequaliser→pushout {in1 = in1} {in2} {f} {g} {e} cp cq = po where
    open is-pushout
    module cq = is-coequaliser cq
    module cp = is-coproduct cp

    po : is-pushout C _ _ _ _
    po .square = sym (assoc _ _ _) βˆ™ cq.coequal βˆ™ assoc _ _ _
    po .universal {i₁' = i₁'} {iβ‚‚'} p =
      cq.universal {e' = cp.[ i₁' , iβ‚‚' ]} (
        cp.[ i₁' , iβ‚‚' ] ∘ (in1 ∘ f) β‰‘βŸ¨ pulll cp.[]βˆ˜ΞΉβ‚ βŸ©β‰‘
        i₁' ∘ f                      β‰‘βŸ¨ p βŸ©β‰‘
        iβ‚‚' ∘ g                      β‰‘Λ˜βŸ¨ pulll cp.[]βˆ˜ΞΉβ‚‚ βŸ©β‰‘Λ˜
        cp.[ i₁' , iβ‚‚' ] ∘ (in2 ∘ g) ∎
      )
    po .universal∘i₁ = pulll cq.factors βˆ™ cp.[]βˆ˜ΞΉβ‚
    po .universal∘iβ‚‚ = pulll cq.factors βˆ™ cp.[]βˆ˜ΞΉβ‚‚
    po .unique p q =
      cq.unique ((cp.unique (sym (assoc _ _ _) βˆ™ p) (sym (assoc _ _ _) βˆ™ q)))

Thus, if a category has an initial object, binary coproducts, and binary coequalisers, it is finitely cocomplete.

  with-coequalisers
    : Initial C
    β†’ (βˆ€ A B β†’ Coproduct C A B)
    β†’ (βˆ€ {A B} (f g : Hom A B) β†’ Coequaliser C f g)
    β†’ Finitely-cocomplete
  with-coequalisers init copr coeq .initial      = init
  with-coequalisers init copr coeq .coproducts   = copr
  with-coequalisers init copr coeq .coequalisers = coeq
  with-coequalisers init copr coeq .pushouts {A} {B} {X} f g =
    record { has-is-po = coproduct-coequaliser→pushout Copr.has-is-coproduct Coequ.has-is-coeq }
    where
      module Copr = Coproduct (copr A B)
      module Coequ = Coequaliser (coeq (Copr.ι₁ ∘ f) (Copr.ΞΉβ‚‚ ∘ g))

With pushoutsπŸ”—

A coproduct is a pushout under a span whose vertex is the initial object.

  initial-pushout→coproduct
    : βˆ€ {P X Y I} {in1 : Hom X P} {in2 : Hom Y P} {f : Hom I X} {g : Hom I Y}
    β†’ is-initial C I β†’ is-pushout C f in1 g in2 β†’ is-coproduct C in1 in2
  initial-pushout→coproduct {in1 = in1} {in2} {f} {g} init po = coprod where
      module Po = is-pushout po

      coprod : is-coproduct C in1 in2
      coprod .is-coproduct.[_,_] in1' in2' =
        Po.universal {i₁' = in1'} {iβ‚‚' = in2'} (is-contrβ†’is-prop (init _) _ _)
      coprod .is-coproduct.[]βˆ˜ΞΉβ‚ = Po.universal∘i₁
      coprod .is-coproduct.[]βˆ˜ΞΉβ‚‚ = Po.universal∘iβ‚‚
      coprod .is-coproduct.unique p q = Po.unique p q

  with-pushouts
    : Initial C
    β†’ (βˆ€ {A B X} (f : Hom X A) (g : Hom X B) β†’ Pushout C f g)
    β†’ Finitely-cocomplete
  with-pushouts bot po = fcc where
    module bot = Initial bot
    mkcoprod : βˆ€ A B β†’ Coproduct C A B
    mkcoprod A B = record { has-is-coproduct = initial-pushoutβ†’coproduct bot.hasβŠ₯ po' }
      where po' = po (bot.hasβŠ₯ A .centre) (bot.hasβŠ₯ B .centre) .Pushout.has-is-po

    mkcoeq : βˆ€ {A B} (f g : Hom A B) β†’ Coequaliser C f g
    mkcoeq {A = A} {B} f g = coequ where

The construction of coequalisers from pushouts follows its dual.

      coequ : Coequaliser C f g
      coequ .coapex = Po.coapex
      coequ .coeq = Po.i₁
      coequ .has-is-coeq .coequal =
        Po.i₁ ∘ f                  β‰‘Λ˜βŸ¨ ap (Po.i₁ ∘_) A+A.[]βˆ˜ΞΉβ‚ βŸ©β‰‘Λ˜
        Po.i₁ ∘ [f,g] ∘ A+A.ι₁     β‰‘βŸ¨ assoc _ _ _ βˆ™ ap (_∘ A+A.ι₁) Po.square βŸ©β‰‘
        (Po.iβ‚‚ ∘ [id,id]) ∘ A+A.ι₁ β‰‘βŸ¨ sym (assoc _ _ _) βˆ™ pushr (A+A.[]βˆ˜ΞΉβ‚ βˆ™ sym A+A.[]βˆ˜ΞΉβ‚‚) βŸ©β‰‘
        (Po.iβ‚‚ ∘ [id,id]) ∘ A+A.ΞΉβ‚‚ β‰‘βŸ¨ ap (_∘ A+A.ΞΉβ‚‚) (sym Po.square) βŸ©β‰‘
        (Po.i₁ ∘ [f,g]) ∘ A+A.ΞΉβ‚‚   β‰‘βŸ¨ sym (assoc _ _ _) βˆ™ ap (Po.i₁ ∘_) A+A.[]βˆ˜ΞΉβ‚‚ βŸ©β‰‘
        Po.i₁ ∘ g                  ∎
      coequ .has-is-coeq .universal {e' = e'} p =
        Po.universal (A+A.uniqueβ‚‚ refl refl (in1) (in2))
        where
          in1 : ((e' ∘ f) ∘ [id,id]) ∘ A+A.ι₁ ≑ (e' ∘ [f,g]) ∘ A+A.ι₁
          in1 =
            ((e' ∘ f) ∘ [id,id]) ∘ A+A.ι₁ β‰‘βŸ¨ cancelr A+A.[]βˆ˜ΞΉβ‚ βŸ©β‰‘ -- β‰‘βŸ¨ cancell A+A.[]βˆ˜ΞΉβ‚ ⟩
            e' ∘ f                        β‰‘Λ˜βŸ¨ pullr A+A.[]βˆ˜ΞΉβ‚ βŸ©β‰‘Λ˜ -- β‰‘Λ˜βŸ¨ pulll A+A.[]βˆ˜ΞΉβ‚ ⟩
            (e' ∘ [f,g]) ∘ A+A.ι₁         ∎

          in2 : ((e' ∘ f) ∘ [id,id]) ∘ A+A.ΞΉβ‚‚ ≑ (e' ∘ [f,g]) ∘ A+A.ΞΉβ‚‚
          in2 =
            ((e' ∘ f) ∘ [id,id]) ∘ A+A.ΞΉβ‚‚ β‰‘βŸ¨ cancelr A+A.[]βˆ˜ΞΉβ‚‚ βŸ©β‰‘
            e' ∘ f                        β‰‘βŸ¨ p βŸ©β‰‘
            e' ∘ g                        β‰‘Λ˜βŸ¨ pullr A+A.[]βˆ˜ΞΉβ‚‚ βŸ©β‰‘Λ˜
            (e' ∘ [f,g]) ∘ A+A.ΞΉβ‚‚         ∎

      coequ .has-is-coeq .factors = Po.universal∘i₁
      coequ .has-is-coeq .unique {F} {e' = e'} {colim = colim} e'=col∘i₁ =
        Po.unique e'=col∘i₁ path
        where
          path : colim ∘ Po.iβ‚‚ ≑ e' ∘ f
          path =
            colim ∘ Po.iβ‚‚                        β‰‘βŸ¨ insertr A+A.[]βˆ˜ΞΉβ‚ βŸ©β‰‘
            ((colim ∘ Po.iβ‚‚) ∘ [id,id]) ∘ A+A.ι₁ β‰‘βŸ¨ ap (_∘ A+A.ι₁) (extendr (sym Po.square)) βŸ©β‰‘
            ((colim ∘ Po.i₁) ∘ [f,g]) ∘ A+A.ι₁   β‰‘βŸ¨ ap (_∘ A+A.ι₁) (ap (_∘ [f,g]) e'=col∘i₁) βŸ©β‰‘
            (e' ∘ [f,g]) ∘ A+A.ι₁                β‰‘βŸ¨ pullr A+A.[]βˆ˜ΞΉβ‚ βŸ©β‰‘
            e' ∘ f           ∎

    fcc : Finitely-cocomplete
    fcc .initial      = bot
    fcc .coproducts   = mkcoprod
    fcc .coequalisers = mkcoeq
    fcc .pushouts     = po

Rex functorsπŸ”—

A right exact, or rex, functor is a functor that preserves finite colimits.

  record is-rex (F : Functor C D) : Type (o βŠ” β„“ βŠ” o' βŠ” β„“') where
    private module F = Functor F

    field
      pres-βŠ₯ : βˆ€ {I} β†’ is-initial C I β†’ is-initial D (F.β‚€ I)
      pres-pushout
        : βˆ€ {P X Y Z} {in1 : C.Hom X P} {in2 : C.Hom Y P}
            {f : C.Hom Z X} {g : C.Hom Z Y}
        β†’ is-pushout C f in1 g in2
        β†’ is-pushout D (F.₁ f) (F.₁ in1) (F.₁ g) (F.₁ in2)
    pres-coproduct
      : βˆ€ {P A B I} {in1 : C.Hom A P} {in2 : C.Hom B P}
      β†’ is-initial C I
      β†’ is-coproduct C in1 in2
      β†’ is-coproduct D (F.₁ in1) (F.₁ in2)
    pres-coproduct  init copr = initial-pushoutβ†’coproduct D (pres-βŠ₯ init)
      (pres-pushout {f = init _ .centre} {g = init _ .centre}
        (coproduct→initial-pushout C init copr))
    pres-epis : βˆ€ {A B} {f : C.Hom A B} β†’ C.is-epic f β†’ D.is-epic (F.₁ f)
    pres-epis {f = f} epi = is-pushout→is-epic
      (subst (Ξ» x β†’ is-pushout D _ x _ x) F.F-id
        (pres-pushout
          (is-epic→is-pushout epi)))