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 _ _ _)
External links
- Sum at Wikidata
Recent changes
- 2025-06-03. Louis Wasserman. Sums and products over arbitrary finite types (#1367).