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