open import Algebra.Group.NAry
open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Abelian.Base
open import Cat.Prelude

open import Data.Fin.Base

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))    β