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 colimits of discrete diagrams of shape .
module _ {I : Type β'} (i-is-grpd : is-groupoid I) (F : I β C.Ob) where open _=>_ InjβCocone : β {x} β (β i β C.Hom (F i) x) β Disc-adjunct {C = C} {iss = i-is-grpd} F => Const x InjβCocone inj .Ξ· i = inj i InjβCocone inj .is-natural i j p = J (Ξ» j p β inj j C.β subst (C.Hom (F i) β F) p C.id β‘ C.id C.β inj i) (C.elimr (transport-refl C.id) β sym (C.idl _)) p is-indexed-coproductβis-colimit : β {x} {inj : β i β C.Hom (F i) x} β is-indexed-coproduct F inj β is-colimit (Disc-adjunct F) x (InjβCocone inj) is-indexed-coproductβis-colimit {x = x} {inj} ic = to-is-colimitp mc refl where module ic = is-indexed-coproduct ic open make-is-colimit mc : make-is-colimit (Disc-adjunct F) x mc .Ο i = inj i mc .commutes {i} {j} p = J (Ξ» j p β inj j C.β subst (C.Hom (F i) β F) p C.id β‘ inj i) (C.elimr (transport-refl C.id)) p mc .universal eta p = ic.match eta mc .factors eta p = ic.commute mc .unique eta p other q = ic.unique eta q is-colimitβis-indexed-coprduct : β {K : Functor β€Cat C} β {eps : Disc-adjunct {iss = i-is-grpd} F => K Fβ !F} β is-lan !F (Disc-adjunct F) K eps β is-indexed-coproduct F (eps .Ξ·) is-colimitβis-indexed-coprduct {K = K} {eps} colim = ic where module colim = is-colimit colim open is-indexed-coproduct ic : is-indexed-coproduct F (eps .Ξ·) ic .match k = colim.universal k (J (Ξ» j p β k j C.β subst (C.Hom (F _) β F) p C.id β‘ k _) (C.elimr (transport-refl _))) ic .commute = colim.factors _ _ ic .unique k comm = colim.unique _ _ _ comm ICβColimit : Indexed-coproduct F β Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F) ICβColimit ic = to-colimit (is-indexed-coproductβis-colimit has-is-ic) where open Indexed-coproduct ic ColimitβIC : Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F) β Indexed-coproduct F ColimitβIC colim .Indexed-coproduct.Ξ£F = _ ColimitβIC colim .Indexed-coproduct.ΞΉ = _ ColimitβIC colim .Indexed-coproduct.has-is-ic = is-colimitβis-indexed-coprduct (Colimit.has-colimit colim)
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