open import Cat.Diagram.Colimit.Base open import Cat.Instances.Discrete open import Cat.Diagram.Pullback open import Cat.Diagram.Initial open import Cat.Prelude module Cat.Diagram.Coproduct.Indexed {o β} (C : Precategory o β) where
Indexed coproductsπ
Indexed coproducts are the dual notion to indexed products, so see there for motivation and exposition.
record is-indexed-coproduct (F : Idx β C.Ob) (ΞΉ : β i β C.Hom (F i) S) : Type (o β β β level-of Idx) where no-eta-equality field match : β {Y} β (β i β C.Hom (F i) Y) β C.Hom S Y commute : β {i} {Y} {f : β i β C.Hom (F i) Y} β match f C.β ΞΉ i β‘ f i unique : β {Y} {h : C.Hom S Y} (f : β i β C.Hom (F i) Y) β (β i β h C.β ΞΉ i β‘ f i) β h β‘ match f eta : β {Y} (h : C.Hom S Y) β h β‘ match (Ξ» i β h C.β ΞΉ i) eta h = unique _ Ξ» _ β refl hom-iso : β {Y} β C.Hom S Y β (β i β C.Hom (F i) Y) hom-iso = (Ξ» z i β z C.β ΞΉ i) , is-isoβis-equiv Ξ» where .is-iso.inv β match .is-iso.rinv x β funext Ξ» i β commute .is-iso.linv x β sym (unique _ Ξ» _ β refl)
A category admits indexed coproducts (of level ) if, for any type and family , there is an indexed coproduct of .
record Indexed-coproduct (F : Idx β C.Ob) : Type (o β β β level-of Idx) where no-eta-equality field {Ξ£F} : C.Ob ΞΉ : β i β C.Hom (F i) Ξ£F has-is-ic : is-indexed-coproduct F ΞΉ open is-indexed-coproduct has-is-ic public has-indexed-coproducts : β β β Type _ has-indexed-coproducts β = β {I : Type β} (F : I β C.Ob) β Indexed-coproduct F
As colimitsπ
Similarly to the product case, when is a groupoid, indexed coproducts correspond to discrete diagrams of shape .
module _ {I : Type β'} (i-is-grpd : is-groupoid I) (F : I β C.Ob) where open Cocone-hom open Initial open Cocone ICβColimit : Indexed-coproduct F β Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F) ICβColimit IC = colim where module IC = Indexed-coproduct IC thecolim : Cocone _ thecolim .coapex = IC.Ξ£F thecolim .Ο = IC.ΞΉ thecolim .commutes {x} = J (Ξ» y p β IC.ΞΉ y C.β subst (C.Hom (F x) β F) p C.id β‘ IC.ΞΉ x) (C.elimr (transport-refl _)) colim : Colimit _ colim .bot = thecolim colim .hasβ₯ x .centre .hom = IC.match (x .Ο) colim .hasβ₯ x .centre .commutes o = IC.commute colim .hasβ₯ x .paths h = Cocone-hom-path _ (sym (IC.unique _ Ξ» i β h .commutes _)) module _ {I : Type β'} (isg : is-groupoid I) (F : Functor (Disc I isg) C) where private module F = Functor F open is-indexed-coproduct open Indexed-coproduct open Cocone-hom open Initial open Cocone InjβCocone : β {Y} β (β i β C.Hom (F.β i) Y) β Cocone F InjβCocone f .coapex = _ InjβCocone f .Ο = f InjβCocone f .commutes {x} = J (Ξ» y p β f y C.β F.β p β‘ f x) (C.elimr F.F-id) ColimitβIC : Colimit {C = C} F β Indexed-coproduct F.β ColimitβIC colim = the-ic where module colim = Cocone (colim .bot) the-ic : Indexed-coproduct _ the-ic .Ξ£F = colim.coapex the-ic .ΞΉ = colim.Ο the-ic .has-is-ic .match f = colim .hasβ₯ (InjβCocone f) .centre .hom the-ic .has-is-ic .commute = colim .hasβ₯ _ .centre .commutes _ the-ic .has-is-ic .unique {h = h} f p i = colim .hasβ₯ (InjβCocone f) .paths hβ² (~ i) .hom where hβ² : Cocone-hom _ _ _ hβ² .hom = h hβ² .commutes o = p _
Disjoint coproductsπ
An indexed coproduct is said to be disjoint if every one of its inclusions is monic, and, for unequal , the square below is a pullback with initial apex. Since the maps are monic, the pullback below computes the intersection of and as subobjects of , hence the name disjoint coproduct: If is an initial object, then .
record is-disjoint-coproduct (F : Idx β C.Ob) (ΞΉ : β i β C.Hom (F i) S) : Type (o β β β level-of Idx) where field is-coproduct : is-indexed-coproduct F ΞΉ injections-are-monic : β i β C.is-monic (ΞΉ i) summands-intersect : β i j β Pullback C (ΞΉ i) (ΞΉ j) different-images-are-disjoint : β i j β Β¬ i β‘ j β is-initial C (summands-intersect i j .Pullback.apex)
Initial objects are disjointπ
We prove that if is an initial object, then it is also an indexed coproduct β for any family β and furthermore, it is a disjoint coproduct.
is-initialβis-disjoint-coproduct : β {β } {F : β₯ β C.Ob} {i : β i β C.Hom (F i) β } β is-initial C β β is-disjoint-coproduct F i is-initialβis-disjoint-coproduct {F = F} {i = i} init = is-disjoint where open is-indexed-coproduct is-coprod : is-indexed-coproduct F i is-coprod .match _ = init _ .centre is-coprod .commute {i = i} = absurd i is-coprod .unique {h = h} f p i = init _ .paths h (~ i) open is-disjoint-coproduct is-disjoint : is-disjoint-coproduct F i is-disjoint .is-coproduct = is-coprod is-disjoint .injections-are-monic i = absurd i is-disjoint .summands-intersect i j = absurd i is-disjoint .different-images-are-disjoint i j p = absurd i