module Cat.Abelian.NAry {o β„“} {C : Precategory o β„“} (A : Ab-category C) where

n-Ary operations on Hom-groupsπŸ”—

We instantiate the theory of n-ary sums in a group to the special case of the abelian groups of an category. In particular, we show that the linearity of function composition extends to distribution over arbitrary sums.

private module A = Ab-category A

βˆ‘β‚• : βˆ€ {x y} n β†’ (Fin n β†’ A.Hom x y) β†’ A.Hom x y
βˆ‘β‚• n f = βˆ‘ {n = n} (Abelianβ†’Group-on (A.Abelian-group-on-hom _ _)) f

βˆ‘-∘-left : βˆ€ {j} {A B C} (f : Fin j β†’ A.Hom A B) {g : A.Hom B C}
          β†’ g A.∘ βˆ‘β‚• j f
          ≑ βˆ‘β‚• j (Ξ» i β†’ g A.∘ f i)
βˆ‘-∘-left {zero} f  = A.∘-zero-r
βˆ‘-∘-left {suc j} f {g = g} =
  g A.∘ (f 0 A.+ βˆ‘β‚• j (Ξ» i β†’ f (fsuc i)))         β‰‘Λ˜βŸ¨ A.∘-linear-r _ _ _ βŸ©β‰‘Λ˜
  g A.∘ f 0 A.+ ⌜ g A.∘ βˆ‘β‚• j (Ξ» i β†’ f (fsuc i)) ⌝ β‰‘βŸ¨ ap! (βˆ‘-∘-left {j} _) βŸ©β‰‘
  g A.∘ f 0 A.+ βˆ‘β‚• j (Ξ» i β†’ g A.∘ f (fsuc i))     ∎

βˆ‘-∘-right : βˆ€ {j} {A B C} (f : Fin j β†’ A.Hom B C) {g : A.Hom A B}
        β†’ βˆ‘β‚• j f A.∘ g
        ≑ βˆ‘β‚• j (Ξ» i β†’ f i A.∘ g)
βˆ‘-∘-right {zero} f      = A.∘-zero-l
βˆ‘-∘-right {suc j} f {g} =
  (f 0 A.+ βˆ‘β‚• j (Ξ» i β†’ f (fsuc i))) A.∘ g          β‰‘Λ˜βŸ¨ A.∘-linear-l _ _ _ βŸ©β‰‘Λ˜
  f 0 A.∘ g A.+ ⌜ βˆ‘β‚• j (Ξ» i β†’ f (fsuc i)) A.∘ g ⌝  β‰‘βŸ¨ ap! (βˆ‘-∘-right {j} _) βŸ©β‰‘
  (f 0 A.∘ g A.+ βˆ‘β‚• j (Ξ» i β†’ f (fsuc i) A.∘ g))    ∎