module Cat.Diagram.Coproduct.Copower where

CopowersπŸ”—

Let C\mathcal{C} be a category admitting ΞΊ\kappa-small indexed coproducts, for example a ΞΊ\kappa-cocomplete category. In the same way that (in ordinary arithmetic) the iterated product of a bunch of copies of the same factor

aΓ—aΓ—β‹―Γ—a⏟n \underbrace{a \times a \times \dots \times a}_{n}

is called a β€œpower”, we refer to the coproduct ∐XA\coprod_{X} A of many copies of an object XX indexed by a ΞΊ\kappa-small set XX as the copower of AA by XX, and alternatively denote it XβŠ—AX \otimes A. If C\mathcal{C} does indeed admit coproducts indexed by any ΞΊ\kappa-small set, then the copowering construction extends to a functor SetsΞΊΓ—Cβ†’C\mathbf{Sets}_\kappa \times \mathcal{C} \to \mathcal{C}.

The notion of copowering gives us slick terminology for a category which admits all ΞΊ\kappa-small coproducts, but not necessarily all ΞΊ\kappa-small colimits: Such a category is precisely one copowered over SetsΞΊ\mathbf{Sets}_\kappa.

  _βŠ—_ : Set β„“ β†’ Ob β†’ Ob
  X βŠ— A = coprods X (Ξ» _ β†’ A) .Ξ£F

Copowers satisfy a universal property: XβŠ—AX \otimes A is a representing object for the functor that takes an object BB to the XXth power of the set of morphisms from AA to BB; in other words, we have a natural isomorphism HomC(XβŠ—A,βˆ’)β‰…HomSets(X,HomC(A,βˆ’))\mathbf{Hom}_\mathcal{C}(X \otimes A, -) \cong \mathbf{Hom}_{\mathbf{Sets}}(X, \mathbf{Hom}_\mathcal{C}(A, -)).

  copower-hom-iso
    : βˆ€ {X A}
    β†’ Hom-from C (X βŠ— A) ≅ⁿ Hom-from (Sets β„“) X F∘ Hom-from C A
  copower-hom-iso {X} {A} = isoβ†’isoⁿ
    (λ _ → equiv→iso (hom-iso (coprods X (λ _ → A))))
    (Ξ» _ β†’ ext Ξ» _ _ β†’ assoc _ _ _)

The action of the copowering functor is given by simultaneously changing the indexing along a function of sets f:X→Yf : X \to Y and changing the underlying object by a morphism g:A→Bg : A \to B. This is functorial by the uniqueness properties of colimiting maps.

  Copowering : Functor (Sets β„“ Γ—αΆœ C) C
  Copowering .Fβ‚€ (X , A) = X βŠ— A
  Copowering .F₁ {X , A} {Y , B} (idx , obj) =
    coprods X (Ξ» _ β†’ A) .match Ξ» i β†’ coprods Y (Ξ» _ β†’ B) .ΞΉ (idx i) ∘ obj
  Copowering .F-id {X , A} = sym $
    coprods X (Ξ» _ β†’ A) .unique _ Ξ» i β†’ sym id-comm
  Copowering .F-∘ {X , A} f g = sym $
    coprods X (Ξ» _ β†’ A) .unique _ Ξ» i β†’
      pullr (coprods _ _ .commute) βˆ™ extendl (coprods _ _ .commute)

cocomplete→copowering
  : βˆ€ {o β„“} {C : Precategory o β„“}
  β†’ is-cocomplete β„“ β„“ C β†’ Functor (Sets β„“ Γ—αΆœ C) C
cocomplete→copowering colim = Copowers.Copowering λ S F →
  Colimit→IC _ (is-hlevel-suc 2 (S .is-tr)) F (colim _)