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

open import Cat.Prelude

open import Data.Fin

module Algebra.Group.NAry where


# n-Ary sumsπ

An important property of abelian groups (really, of abelian monoids, but we will only need them for groups) is that their binary operation extends cleanly to an βn-aryβ operation, where the niceness of the extension is guaranteed by associativity. For a group we define the sum of an sequence of elements to be the sum βfrom the leftβ: add the first element then keep going.

β : β {n} {β} {T : Type β} (G : Group-on T) β (Fin n β T) β T
β {n = zero} G x  = Group-on.unit G
β {n = suc n} G x = Group-on._β_ G (x fzero) (β G Ξ» e β x (fsuc e))

β-path : β {n} {β} {T : Type β} (G : Group-on T) {f g : Fin n β T}
β (β i β f i β‘ g i)
β β G f β‘ β G g
β-path G p = ap (β G) (funext p)

β-zero
: β {n} {β} {T : Type β} (G : Group-on T)
β β {n} G (Ξ» e β Group-on.unit G) β‘ Group-on.unit G
β-zero {n = zero} G = refl
β-zero {n = suc n} G = Group-on.idl G β β-zero {n} G

module _ {β} {T : Type β} (G : Abelian-group-on T) where
private
module G = Abelian-group-on G
G' = AbelianβGroup-on G


Our assumption that is abelian comes in when we want to prove that

  β-split : β {n} (f : Fin n β T) (g : Fin n β T)
β β G' (Ξ» i β f i G.* g i) β‘ (β G' f G.* β G' g)
β-split {zero} f g = sym G.idl
β-split {suc n} f g =
(f fzero G.* g fzero) G.* β G' (Ξ» i β f (fsuc i) G.* g (fsuc i))              β‘β¨ apβ G._*_ refl (β-split (Ξ» e β f (fsuc e)) (Ξ» e β g (fsuc e))) β©β‘
(f fzero G.* g fzero) G.* β G' (Ξ» e β f (fsuc e)) G.* β G' (Ξ» e β g (fsuc e)) β‘β¨ G.pullr (G.extendl G.commutes) β©β‘
f fzero G.* β G' (Ξ» e β f (fsuc e)) G.* g fzero G.* β G' (Ξ» e β g (fsuc e))   β‘β¨ G.associative β©β‘
(f fzero G.* β G' (Ξ» e β f (fsuc e))) G.* g fzero G.* β G' (Ξ» e β g (fsuc e)) β


A trivial-looking, but very convenient result1 lets us reduce a sum to a single element, as long as the function weβre defining has non-zero values at every other index. Put another way: if is such that but everywhere else, then

module _ {β} {T : Type β} (G : Group-on T)  where
private module G = Group-on G
β-diagonal-lemma
: β {n} (i : Fin n) {x : T}
β (f : Fin n β T)
β f i β‘ x
β (β j β Β¬ i β‘ j β f j β‘ G.unit)
β β G f β‘ x
β-diagonal-lemma {suc n} fzero f f0=x fj=0 =
G.elimr ( β-path {n = n} G (Ξ» i β fj=0 (fsuc i) fzeroβ fsuc)
β β-zero {n = n} G) β f0=x
β-diagonal-lemma {suc n} (fsuc i) {x} f fj=x fβ i=0 =
f fzero G.β β {n} G (Ξ» e β f (fsuc e)) β‘β¨ G.eliml (fβ i=0 fzero Ξ» e β fzeroβ fsuc (sym e)) β©β‘
β {n} G (Ξ» e β f (fsuc e))             β‘β¨ β-diagonal-lemma {n} i (Ξ» e β f (fsuc e)) fj=x (Ξ» j iβ j β fβ i=0 (fsuc j) (Ξ» e β iβ j (fsuc-inj e))) β©β‘
x                                      β


1. which, additionally, is hard to re-derive on a case-by-case basisβ©οΈ