open import Cat.Diagram.Colimit.Base open import Cat.Diagram.Coequaliser open import Cat.Diagram.Coproduct open import Cat.Diagram.Initial open import Cat.Diagram.Pushout open import Cat.Prelude import Cat.Reasoning as Cat 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. 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 .colimiting {iββ² = iββ²} {iββ²} p = cq.coequalise {eβ² = cp.[ iββ² , iββ² ]} ( cp.[ iββ² , iββ² ] β (in1 β f) β‘β¨ pulll cp.inββfactor β©β‘ iββ² β f β‘β¨ p β©β‘ iββ² β g β‘Λβ¨ pulll cp.inββfactor β©β‘Λ cp.[ iββ² , iββ² ] β (in2 β g) β ) po .iββcolimiting = pulll cq.universal β cp.inββfactor po .iββcolimiting = pulll cq.universal β cp.inββfactor po .unique p q = cq.unique (sym (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.inβ β f) (Copr.inβ β 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.colimiting {iββ² = in1β²} {iββ² = in2β²} (is-contrβis-prop (init _) _ _) coprod .is-coproduct.inββfactor = Po.iββcolimiting coprod .is-coproduct.inββfactor = Po.iββcolimiting coprod .is-coproduct.unique other 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.inββfactor β©β‘Λ Po.iβ β [f,g] β A+A.inβ β‘β¨ assoc _ _ _ β ap (_β A+A.inβ) Po.square β©β‘ (Po.iβ β [id,id]) β A+A.inβ β‘β¨ sym (assoc _ _ _) β pushr (A+A.inββfactor β sym A+A.inββfactor) β©β‘ (Po.iβ β [id,id]) β A+A.inβ β‘β¨ ap (_β A+A.inβ) (sym Po.square) β©β‘ (Po.iβ β [f,g]) β A+A.inβ β‘β¨ sym (assoc _ _ _) β ap (Po.iβ β_) A+A.inββfactor β©β‘ Po.iβ β g β coequ .has-is-coeq .coequalise {eβ² = eβ²} p = Po.colimiting (A+A.uniqueβ _ refl refl _ (in1) (in2)) where in1 : ((eβ² β f) β [id,id]) β A+A.inβ β‘ (eβ² β [f,g]) β A+A.inβ in1 = ((eβ² β f) β [id,id]) β A+A.inβ β‘β¨ cancelr A+A.inββfactor β©β‘ -- β‘β¨ cancell A+A.inββfactor β© eβ² β f β‘Λβ¨ pullr A+A.inββfactor β©β‘Λ -- β‘Λβ¨ pulll A+A.inββfactor β© (eβ² β [f,g]) β A+A.inβ β in2 : ((eβ² β f) β [id,id]) β A+A.inβ β‘ (eβ² β [f,g]) β A+A.inβ in2 = ((eβ² β f) β [id,id]) β A+A.inβ β‘β¨ cancelr A+A.inββfactor β©β‘ eβ² β f β‘β¨ p β©β‘ eβ² β g β‘Λβ¨ pullr A+A.inββfactor β©β‘Λ (eβ² β [f,g]) β A+A.inβ β coequ .has-is-coeq .universal = Po.iββcolimiting coequ .has-is-coeq .unique {F} {eβ² = eβ²} {colim = colim} eβ²=colβiβ = Po.unique (sym eβ²=colβiβ) path where path : colim β Po.iβ β‘ eβ² β f path = colim β Po.iβ β‘β¨ insertr A+A.inββfactor β©β‘ ((colim β Po.iβ) β [id,id]) β A+A.inβ β‘β¨ ap (_β A+A.inβ) (extendr (sym Po.square)) β©β‘ ((colim β Po.iβ) β [f,g]) β A+A.inβ β‘β¨ ap (_β A+A.inβ) (ap (_β [f,g]) (sym eβ²=colβiβ)) β©β‘ (eβ² β [f,g]) β A+A.inβ β‘β¨ pullr A+A.inββfactor β©β‘ 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))