Sums of finite families of elements in commutative semigroups
Content created by Louis Wasserman.
Created on 2025-08-31.
Last modified on 2025-08-31.
{-# OPTIONS --lossy-unification #-} module group-theory.sums-of-finite-families-of-elements-commutative-semigroups 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.dependent-pair-types open import foundation.empty-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.sets open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-empty-type open import foundation.type-arithmetic-unit-type open import foundation.unit-type open import foundation.universal-property-propositional-truncation-into-sets open import foundation.universe-levels open import group-theory.commutative-semigroups open import group-theory.sums-of-finite-sequences-of-elements-commutative-semigroups open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.coproducts-inhabited-finite-types open import univalent-combinatorics.counting open import univalent-combinatorics.counting-dependent-pair-types open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.double-counting open import univalent-combinatorics.finite-types open import univalent-combinatorics.inhabited-finite-types open import univalent-combinatorics.standard-finite-types
Idea
The
sum operation¶
extends the binary operation on a
commutative semigroup G to any
family of elements of G indexed by an
inhabited finite type.
We use additive terminology consistently with the linear algebra definition of finite sequences in commutative semigroups despite the use of multiplicative terminology for commutative semigroups in general.
Sums over counted types
Definition
sum-count-Commutative-Semigroup : {l1 l2 : Level} (G : Commutative-Semigroup l1) (A : UU l2) → is-inhabited A → count A → (A → type-Commutative-Semigroup G) → type-Commutative-Semigroup G sum-count-Commutative-Semigroup G A |A| cA@(zero-ℕ , _) _ = ex-falso ( is-nonempty-is-inhabited ( |A|) ( is-empty-is-zero-number-of-elements-count cA refl)) sum-count-Commutative-Semigroup G A _ (succ-ℕ n , Fin-sn≃A) f = sum-fin-sequence-type-Commutative-Semigroup G n (f ∘ map-equiv Fin-sn≃A)
Properties
Sums for a counted type are homotopy invariant
module _ {l1 l2 : Level} (G : Commutative-Semigroup l1) (A : UU l2) (|A| : is-inhabited A) where htpy-sum-count-Commutative-Semigroup : (c : count A) → {f g : A → type-Commutative-Semigroup G} → (f ~ g) → sum-count-Commutative-Semigroup G A |A| c f ＝ sum-count-Commutative-Semigroup G A |A| c g htpy-sum-count-Commutative-Semigroup cA@(zero-ℕ , _) _ = ex-falso ( is-nonempty-is-inhabited ( |A|) ( is-empty-is-zero-number-of-elements-count cA refl)) htpy-sum-count-Commutative-Semigroup (succ-ℕ nA , _) H = htpy-sum-fin-sequence-type-Commutative-Semigroup G nA (λ i → H _)
Two counts for the same type produce equal sums
module _ {l1 l2 : Level} (G : Commutative-Semigroup l1) (A : UU l2) (|A| : is-inhabited A) where abstract eq-sum-count-equiv-Commutative-Semigroup : (n : ℕ) → (equiv1 equiv2 : Fin (succ-ℕ n) ≃ A) → (f : A → type-Commutative-Semigroup G) → sum-count-Commutative-Semigroup G A |A| (succ-ℕ n , equiv1) f ＝ sum-count-Commutative-Semigroup G A |A| (succ-ℕ n , equiv2) f eq-sum-count-equiv-Commutative-Semigroup n equiv1 equiv2 f = equational-reasoning sum-fin-sequence-type-Commutative-Semigroup G n (f ∘ map-equiv equiv1) ＝ sum-fin-sequence-type-Commutative-Semigroup ( G) ( n) ( (f ∘ map-equiv equiv1) ∘ (map-inv-equiv equiv1 ∘ map-equiv equiv2)) by preserves-sum-permutation-fin-sequence-type-Commutative-Semigroup ( G) ( n) ( inv-equiv equiv1 ∘e equiv2) ( f ∘ map-equiv equiv1) ＝ sum-fin-sequence-type-Commutative-Semigroup G n (f ∘ map-equiv equiv2) by ap ( λ g → sum-fin-sequence-type-Commutative-Semigroup ( G) ( n) ( f ∘ (g ∘ map-equiv equiv2))) ( eq-htpy (is-section-map-inv-equiv equiv1)) eq-sum-count-Commutative-Semigroup : (f : A → type-Commutative-Semigroup G) (c1 c2 : count A) → sum-count-Commutative-Semigroup G A |A| c1 f ＝ sum-count-Commutative-Semigroup G A |A| c2 f eq-sum-count-Commutative-Semigroup f c1@(zero-ℕ , _) _ = ex-falso ( is-nonempty-is-inhabited ( |A|) ( is-empty-is-zero-number-of-elements-count c1 refl)) eq-sum-count-Commutative-Semigroup f c1@(succ-ℕ n , e1) c2@(_ , e2) with double-counting c1 c2 ... | refl = eq-sum-count-equiv-Commutative-Semigroup n e1 e2 f
Sums of counted families indexed by equivalent types are equal
module _ {l1 l2 l3 : Level} (G : Commutative-Semigroup l1) (A : UU l2) (|A| : is-inhabited A) (B : UU l3) (|B| : is-inhabited B) (H : A ≃ B) where abstract sum-equiv-count-Commutative-Semigroup : (cA : count A) (cB : count B) (f : A → type-Commutative-Semigroup G) → sum-count-Commutative-Semigroup G A |A| cA f ＝ sum-count-Commutative-Semigroup G B |B| cB (f ∘ map-inv-equiv H) sum-equiv-count-Commutative-Semigroup cA@(zero-ℕ , _) _ _ = ex-falso ( is-nonempty-is-inhabited ( |A|) ( is-empty-is-zero-number-of-elements-count cA refl)) sum-equiv-count-Commutative-Semigroup cA@(succ-ℕ nA , Fin-nA≃A) cB@(_ , Fin-nB≃B) f with double-counting-equiv cA cB H ... | refl = preserves-sum-permutation-fin-sequence-type-Commutative-Semigroup ( G) ( nA) ( inv-equiv Fin-nA≃A ∘e inv-equiv H ∘e Fin-nB≃B) ( _) ∙ htpy-sum-fin-sequence-type-Commutative-Semigroup ( G) ( nA) ( λ i → ap f (is-section-map-inv-equiv Fin-nA≃A _))
Sums of coproducts of counted types
module _ {l1 l2 l3 : Level} (G : Commutative-Semigroup l1) (A : UU l2) (|A| : is-inhabited A) (B : UU l3) (|B| : is-inhabited B) (|A+B| : is-inhabited (A + B)) where abstract distributive-sum-coproduct-count-Commutative-Semigroup : (cA : count A) (cB : count B) → (f : (A + B) → type-Commutative-Semigroup G) → sum-count-Commutative-Semigroup ( G) ( A + B) ( |A+B|) ( count-coproduct cA cB) ( f) ＝ mul-Commutative-Semigroup G ( sum-count-Commutative-Semigroup G A |A| cA (f ∘ inl)) ( sum-count-Commutative-Semigroup G B |B| cB (f ∘ inr)) distributive-sum-coproduct-count-Commutative-Semigroup cA@(succ-ℕ nA , Fin-snA≃A) cB@(succ-ℕ nB , Fin-snB≃B) f = split-sum-fin-sequence-type-Commutative-Semigroup G nA nB _ ∙ ap-mul-Commutative-Semigroup G ( htpy-sum-fin-sequence-type-Commutative-Semigroup G nA ( λ i → ap f (map-equiv-count-coproduct-inl-coproduct-Fin cA cB i))) ( htpy-sum-fin-sequence-type-Commutative-Semigroup G nB ( λ i → ap f (map-equiv-count-coproduct-inr-coproduct-Fin cA cB i))) distributive-sum-coproduct-count-Commutative-Semigroup cA@(zero-ℕ , _) cB@(succ-ℕ _ , _) _ = ex-falso ( is-nonempty-is-inhabited ( |A|) ( is-empty-is-zero-number-of-elements-count cA refl)) distributive-sum-coproduct-count-Commutative-Semigroup cA@(zero-ℕ , _) cB@(zero-ℕ , _) _ = ex-falso ( is-nonempty-is-inhabited ( |A|) ( is-empty-is-zero-number-of-elements-count cA refl)) distributive-sum-coproduct-count-Commutative-Semigroup cA@(succ-ℕ _ , _) cB@(zero-ℕ , _) _ = ex-falso ( is-nonempty-is-inhabited ( |B|) ( is-empty-is-zero-number-of-elements-count cB refl))
Sums over finite types
Definition
module _ {l1 l2 : Level} (G : Commutative-Semigroup l1) (A : Inhabited-Finite-Type l2) where sum-finite-Commutative-Semigroup : (f : type-Inhabited-Finite-Type A → type-Commutative-Semigroup G) → type-Commutative-Semigroup G sum-finite-Commutative-Semigroup f = map-universal-property-set-quotient-trunc-Prop ( set-Commutative-Semigroup G) ( λ c → sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( c) ( f)) ( eq-sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( f)) ( is-finite-Inhabited-Finite-Type A)
Properties
The sum over a finite type is its sum over any count for the type
module _ {l1 l2 : Level} (G : Commutative-Semigroup l1) (A : Inhabited-Finite-Type l2) (cA : count (type-Inhabited-Finite-Type A)) where abstract eq-sum-finite-sum-count-Commutative-Semigroup : (f : type-Inhabited-Finite-Type A → type-Commutative-Semigroup G) → sum-finite-Commutative-Semigroup G A f ＝ sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) cA f eq-sum-finite-sum-count-Commutative-Semigroup f = ap ( λ c → sum-finite-Commutative-Semigroup G ((_ , c) , _) f) ( all-elements-equal-type-trunc-Prop _ _) ∙ htpy-universal-property-set-quotient-trunc-Prop ( set-Commutative-Semigroup G) ( λ c → sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( c) ( f)) ( eq-sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( f)) ( cA)
Sums over a finite type are homotopy invariant
module _ {l1 l2 : Level} (G : Commutative-Semigroup l1) (A : Inhabited-Finite-Type l2) where abstract htpy-sum-finite-Commutative-Semigroup : {f g : type-Inhabited-Finite-Type A → type-Commutative-Semigroup G} → f ~ g → sum-finite-Commutative-Semigroup G A f ＝ sum-finite-Commutative-Semigroup G A g htpy-sum-finite-Commutative-Semigroup {f} {g} H = let open do-syntax-trunc-Prop ( Id-Prop ( set-Commutative-Semigroup G) ( sum-finite-Commutative-Semigroup G A f) ( sum-finite-Commutative-Semigroup G A g)) in do cA ← is-finite-Inhabited-Finite-Type A equational-reasoning sum-finite-Commutative-Semigroup G A f ＝ sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( cA) ( f) by eq-sum-finite-sum-count-Commutative-Semigroup G A cA f ＝ sum-count-Commutative-Semigroup G ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( cA) ( g) by htpy-sum-count-Commutative-Semigroup ( G) ( type-Inhabited-Finite-Type A) ( is-inhabited-type-Inhabited-Finite-Type A) ( cA) ( H) ＝ sum-finite-Commutative-Semigroup G A g by inv (eq-sum-finite-sum-count-Commutative-Semigroup G A cA g)
Sums over finite types are preserved by equivalences
module _ {l1 l2 l3 : Level} (G : Commutative-Semigroup l1) (A : Inhabited-Finite-Type l2) (B : Inhabited-Finite-Type l3) (H : equiv-Inhabited-Finite-Type A B) where abstract sum-equiv-finite-Commutative-Semigroup : (f : type-Inhabited-Finite-Type A → type-Commutative-Semigroup G) → sum-finite-Commutative-Semigroup G A f ＝ sum-finite-Commutative-Semigroup G B (f ∘ map-inv-equiv H) sum-equiv-finite-Commutative-Semigroup f = let open do-syntax-trunc-Prop ( Id-Prop ( set-Commutative-Semigroup G) ( sum-finite-Commutative-Semigroup G A f) ( sum-finite-Commutative-Semigroup G B (f ∘ map-inv-equiv H))) in do cA ← is-finite-Inhabited-Finite-Type A cB ← is-finite-Inhabited-Finite-Type B ( eq-sum-finite-sum-count-Commutative-Semigroup G _ cA f ∙ sum-equiv-count-Commutative-Semigroup G _ _ _ _ H cA cB f ∙ inv (eq-sum-finite-sum-count-Commutative-Semigroup G _ cB _))
Sums over finite types distribute over coproducts
module _ {l1 l2 l3 : Level} (G : Commutative-Semigroup l1) (A : Inhabited-Finite-Type l2) (B : Inhabited-Finite-Type l3) where abstract distributive-distributive-sum-coproduct-finite-Commutative-Semigroup : (f : type-Inhabited-Finite-Type A + type-Inhabited-Finite-Type B → type-Commutative-Semigroup G) → sum-finite-Commutative-Semigroup ( G) ( coproduct-Inhabited-Finite-Type A B) ( f) ＝ mul-Commutative-Semigroup ( G) ( sum-finite-Commutative-Semigroup G A (f ∘ inl)) ( sum-finite-Commutative-Semigroup G B (f ∘ inr)) distributive-distributive-sum-coproduct-finite-Commutative-Semigroup f = let open do-syntax-trunc-Prop ( Id-Prop ( set-Commutative-Semigroup G) ( sum-finite-Commutative-Semigroup ( G) ( coproduct-Inhabited-Finite-Type A B) ( f)) ( mul-Commutative-Semigroup ( G) ( sum-finite-Commutative-Semigroup G A (f ∘ inl)) ( sum-finite-Commutative-Semigroup G B (f ∘ inr)))) in do cA ← is-finite-Inhabited-Finite-Type A cB ← is-finite-Inhabited-Finite-Type B ( eq-sum-finite-sum-count-Commutative-Semigroup ( G) ( coproduct-Inhabited-Finite-Type A B) ( count-coproduct cA cB) ( f) ∙ distributive-sum-coproduct-count-Commutative-Semigroup G _ _ _ _ _ ( cA) ( cB) ( f) ∙ ap-mul-Commutative-Semigroup G ( inv ( eq-sum-finite-sum-count-Commutative-Semigroup G A cA (f ∘ inl))) ( inv ( eq-sum-finite-sum-count-Commutative-Semigroup ( G) ( B) ( cB) ( f ∘ inr))))
External links
- Sum at Wikidata
Recent changes
- 2025-08-31. Louis Wasserman. Commutative semigroups (#1494).