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 .universal {iββ² = iββ²} {iββ²} p = cq.universal {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ββuniversal = pulll cq.factors β cp.inββfactor po .iββuniversal = pulll cq.factors β cp.inββfactor 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.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.universal {iββ² = in1β²} {iββ² = in2β²} (is-contrβis-prop (init _) _ _) coprod .is-coproduct.inββfactor = Po.iββuniversal coprod .is-coproduct.inββfactor = Po.iββuniversal 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.
module A+A = Coproduct (mkcoprod A A) [id,id] : Hom A+A.coapex A [id,id] = A+A.[ id , id ] [f,g] : Hom A+A.coapex B [f,g] = A+A.[ f , g ] module Po = Pushout (po [f,g] [id,id]) open is-coequaliser open Coequaliser
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 .universal {eβ² = eβ²} p = Po.universal (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 .factors = Po.iββuniversal 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.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]) 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
coproductβinitial-pushout : β {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-coproduct C in1 in2 β is-pushout C f in1 g in2 coproductβinitial-pushout i r = po where open is-pushout po : is-pushout C _ _ _ _ po .square = is-contrβis-prop (i _) _ _ po .universal _ = r .is-coproduct.[_,_] _ _ po .iββuniversal = r .is-coproduct.inββfactor po .iββuniversal = r .is-coproduct.inββfactor po .unique p q = r .is-coproduct.unique _ p q
Rex functorsπ
A right exact, or rex, functor is a functor that preserves finite colimits.
module _ {o β oβ² ββ²} {C : Precategory o β} {D : Precategory oβ² ββ²} where private module C = Cat C private module D = Cat D
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)))