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 GG, we define the sum of an nn-ary sequence of GG’s 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

Our assumption that GG is abelian comes in when we want to prove that (βˆ‘f)+(βˆ‘g)=βˆ‘(f+g)(\sum f) + (\sum g) = \sum (f + g):

  βˆ‘-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 (ab _ _)) βŸ©β‰‘
    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 f:[n]β†’Gf : [n] \to G is such that f(i)=xf(i) = x but f(j)=0f(j) = 0 everywhere else, then βˆ‘f=x\sum f = x.

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β†©οΈŽ