Sums of finite sequences of elements in monoids

Content created by Louis Wasserman.

Created on 2025-06-03.
Last modified on 2025-06-03.

module group-theory.sums-of-finite-sequences-of-elements-monoids where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import group-theory.monoids

open import linear-algebra.finite-sequences-in-monoids

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.standard-finite-types

Idea

The sum operation operation extends the binary operation on a monoid M to any finite sequence of elements of M.

Definition

sum-fin-sequence-type-Monoid :
  {l : Level} (M : Monoid l) (n : ) 
  (fin-sequence-type-Monoid M n)  type-Monoid M
sum-fin-sequence-type-Monoid M zero-ℕ f = unit-Monoid M
sum-fin-sequence-type-Monoid M (succ-ℕ n) f =
  mul-Monoid M
    ( sum-fin-sequence-type-Monoid M n (f  inl-Fin n))
    ( f (inr star))

Properties

Sums of one and two elements

module _
  {l : Level} (M : Monoid l)
  where

  compute-sum-one-element-Monoid :
    (f : fin-sequence-type-Monoid M 1) 
    sum-fin-sequence-type-Monoid M 1 f  head-fin-sequence-type-Monoid M 0 f
  compute-sum-one-element-Monoid f =
    left-unit-law-mul-Monoid M (f (inr star))

  compute-sum-two-elements-Monoid :
    (f : fin-sequence-type-Monoid M 2) 
    sum-fin-sequence-type-Monoid M 2 f 
    mul-Monoid M (f (zero-Fin 1)) (f (one-Fin 1))
  compute-sum-two-elements-Monoid f =
    ( associative-mul-Monoid M
      (unit-Monoid M) (f (zero-Fin 1)) (f (one-Fin 1))) 
    ( left-unit-law-mul-Monoid M
      ( mul-Monoid M (f (zero-Fin 1)) (f (one-Fin 1))))

Sums are homotopy invariant

module _
  {l : Level} (M : Monoid l)
  where

  htpy-sum-fin-sequence-type-Monoid :
    (n : ) {f g : fin-sequence-type-Monoid M n} 
    (f ~ g) 
    sum-fin-sequence-type-Monoid M n f  sum-fin-sequence-type-Monoid M n g
  htpy-sum-fin-sequence-type-Monoid zero-ℕ H = refl
  htpy-sum-fin-sequence-type-Monoid (succ-ℕ n) H =
    ap-mul-Monoid M
      ( htpy-sum-fin-sequence-type-Monoid n (H ·r inl-Fin n))
      ( H (inr star))

Sums are equal to the zero-th term plus the rest

module _
  {l : Level} (M : Monoid l)
  where

  cons-sum-fin-sequence-type-Monoid :
    (n : ) (f : fin-sequence-type-Monoid M (succ-ℕ n)) 
    {x : type-Monoid M}  head-fin-sequence-type-Monoid M n f  x 
    sum-fin-sequence-type-Monoid M (succ-ℕ n) f 
    mul-Monoid M (sum-fin-sequence-type-Monoid M n (f  inl-Fin n)) x
  cons-sum-fin-sequence-type-Monoid n f refl = refl

  snoc-sum-fin-sequence-type-Monoid :
    (n : ) (f : fin-sequence-type-Monoid M (succ-ℕ n)) 
    {x : type-Monoid M}  f (zero-Fin n)  x 
    sum-fin-sequence-type-Monoid M (succ-ℕ n) f 
    mul-Monoid M
      ( x)
      ( sum-fin-sequence-type-Monoid M n (f  inr-Fin n))
  snoc-sum-fin-sequence-type-Monoid zero-ℕ f refl =
    ( compute-sum-one-element-Monoid M f) 
    ( inv (right-unit-law-mul-Monoid M (f (zero-Fin 0))))
  snoc-sum-fin-sequence-type-Monoid (succ-ℕ n) f refl =
    ( ap
      ( mul-Monoid' M (head-fin-sequence-type-Monoid M (succ-ℕ n) f))
      ( snoc-sum-fin-sequence-type-Monoid n (f  inl-Fin (succ-ℕ n)) refl)) 
    ( associative-mul-Monoid M
      ( f (zero-Fin (succ-ℕ n)))
      ( sum-fin-sequence-type-Monoid M n (f  (inr-Fin (succ-ℕ n)  inl-Fin n)))
      ( head-fin-sequence-type-Monoid M (succ-ℕ n) f))

Extending a sum of elements in a monoid

module _
  {l : Level} (M : Monoid l)
  where

  extend-sum-fin-sequence-type-Monoid :
    (n : ) (f : fin-sequence-type-Monoid M n) 
    sum-fin-sequence-type-Monoid M
      ( succ-ℕ n)
      ( cons-fin-sequence-type-Monoid M n (unit-Monoid M) f) 
    sum-fin-sequence-type-Monoid M n f
  extend-sum-fin-sequence-type-Monoid n f =
    right-unit-law-mul-Monoid M (sum-fin-sequence-type-Monoid M n f)

Shifting a sum of elements in a monoid

module _
  {l : Level} (M : Monoid l)
  where

  shift-sum-fin-sequence-type-Monoid :
    (n : ) (f : fin-sequence-type-Monoid M n) 
    sum-fin-sequence-type-Monoid M
      ( succ-ℕ n)
      ( snoc-fin-sequence-type-Monoid M n f
        ( unit-Monoid M)) 
    sum-fin-sequence-type-Monoid M n f
  shift-sum-fin-sequence-type-Monoid zero-ℕ f =
    left-unit-law-mul-Monoid M (unit-Monoid M)
  shift-sum-fin-sequence-type-Monoid (succ-ℕ n) f =
    ap
      ( mul-Monoid' M
        ( head-fin-sequence-type-Monoid M n f))
      ( shift-sum-fin-sequence-type-Monoid n
        ( tail-fin-sequence-type-Monoid M n f))

A sum of zeros is zero

module _
  {l : Level} (M : Monoid l)
  where

  abstract
    sum-zero-fin-sequence-type-Monoid :
      (n : ) 
      sum-fin-sequence-type-Monoid M n (zero-fin-sequence-type-Monoid M n) 
      unit-Monoid M
    sum-zero-fin-sequence-type-Monoid zero-ℕ = refl
    sum-zero-fin-sequence-type-Monoid (succ-ℕ n) =
      right-unit-law-mul-Monoid M _  sum-zero-fin-sequence-type-Monoid n

Splitting sums of n + m elements into a sum of n elements and a sum of m elements

split-sum-fin-sequence-type-Monoid :
  {l : Level} (M : Monoid l)
  (n m : ) (f : fin-sequence-type-Monoid M (n +ℕ m)) 
  sum-fin-sequence-type-Monoid M (n +ℕ m) f 
  mul-Monoid M
    ( sum-fin-sequence-type-Monoid M n (f  inl-coproduct-Fin n m))
    ( sum-fin-sequence-type-Monoid M m (f  inr-coproduct-Fin n m))
split-sum-fin-sequence-type-Monoid M n zero-ℕ f =
  inv (right-unit-law-mul-Monoid M (sum-fin-sequence-type-Monoid M n f))
split-sum-fin-sequence-type-Monoid M n (succ-ℕ m) f =
  ( ap
    ( mul-Monoid' M (f (inr star)))
    ( split-sum-fin-sequence-type-Monoid M n m (f  inl))) 
  ( associative-mul-Monoid M _ _ _)
  • Sum at Wikidata

Recent changes