Sums of finite families of elements in commutative semirings

Content created by Louis Wasserman.

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

module commutative-algebra.sums-of-finite-families-of-elements-commutative-semirings where
Imports 
open import commutative-algebra.commutative-semirings
open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semirings

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import finite-group-theory.permutations-standard-finite-types

open import foundation.automorphisms
open import foundation.coproduct-types
open import foundation.empty-types
open import foundation.equivalences
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 linear-algebra.finite-sequences-in-commutative-semirings

open import lists.finite-sequences

open import ring-theory.sums-of-finite-families-of-elements-semirings

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.finite-types

Idea

The sum operation extends the binary addition operation on a commutative semiring R to any finite sequence of elements of R.

Definition

sum-count-Commutative-Semiring :
  {l1 l2 : Level} (R : Commutative-Semiring l1) (A : UU l2) → count A →
  (A → type-Commutative-Semiring R) → type-Commutative-Semiring R
sum-count-Commutative-Semiring R =
  sum-count-Semiring (semiring-Commutative-Semiring R)

sum-finite-Commutative-Semiring :
  {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2) →
  (type-Finite-Type A → type-Commutative-Semiring R) →
  type-Commutative-Semiring R
sum-finite-Commutative-Semiring R =
  sum-finite-Semiring (semiring-Commutative-Semiring R)

Properties

Sums over the unit type

module _
  {l : Level} (A : Commutative-Semiring l)
  where

  sum-unit-finite-Commutative-Semiring :
    (f : unit → type-Commutative-Semiring A) →
    sum-finite-Commutative-Semiring A unit-Finite-Type f ＝ f star
  sum-unit-finite-Commutative-Semiring =
    sum-unit-finite-Semiring (semiring-Commutative-Semiring A)

Sums are homotopy invariant

module _
  {l : Level} (R : Commutative-Semiring l)
  where

  htpy-sum-finite-Commutative-Semiring :
    {l2 : Level} (A : Finite-Type l2) →
    {f g : type-Finite-Type A → type-Commutative-Semiring R} → (f ~ g) →
    sum-finite-Commutative-Semiring R A f ＝
    sum-finite-Commutative-Semiring R A g
  htpy-sum-finite-Commutative-Semiring =
    htpy-sum-finite-Semiring (semiring-Commutative-Semiring R)

Multiplication distributes over sums

module _
  {l : Level} (R : Commutative-Semiring l)
  where

  left-distributive-mul-sum-finite-Commutative-Semiring :
    {l2 : Level} (A : Finite-Type l2) (x : type-Commutative-Semiring R) →
    (f : type-Finite-Type A → type-Commutative-Semiring R) →
    mul-Commutative-Semiring R x (sum-finite-Commutative-Semiring R A f) ＝
    sum-finite-Commutative-Semiring R A (mul-Commutative-Semiring R x ∘ f)
  left-distributive-mul-sum-finite-Commutative-Semiring =
    left-distributive-mul-sum-finite-Semiring (semiring-Commutative-Semiring R)

  right-distributive-mul-sum-finite-Commutative-Semiring :
    {l2 : Level} (A : Finite-Type l2) →
    (f : type-Finite-Type A → type-Commutative-Semiring R) →
    (x : type-Commutative-Semiring R) →
    mul-Commutative-Semiring R (sum-finite-Commutative-Semiring R A f) x ＝
    sum-finite-Commutative-Semiring R A (mul-Commutative-Semiring' R x ∘ f)
  right-distributive-mul-sum-finite-Commutative-Semiring =
    right-distributive-mul-sum-finite-Semiring (semiring-Commutative-Semiring R)

Sums over finite types are preserved by equivalences

module _
  {l1 l2 l3 : Level} (R : Commutative-Semiring l1)
  (A : Finite-Type l2) (B : Finite-Type l3) (H : equiv-Finite-Type A B)
  where

  sum-equiv-finite-Commutative-Semiring :
    (f : type-Finite-Type A → type-Commutative-Semiring R) →
    sum-finite-Commutative-Semiring R A f ＝
    sum-finite-Commutative-Semiring R B (f ∘ map-inv-equiv H)
  sum-equiv-finite-Commutative-Semiring =
    sum-equiv-finite-Semiring (semiring-Commutative-Semiring R) A B H

module _
  {l1 l2 : Level} (R : Commutative-Semiring l1)
  (A : Finite-Type l2) (σ : Aut (type-Finite-Type A))
  where

  sum-aut-finite-Commutative-Semiring :
    (f : type-Finite-Type A → type-Commutative-Semiring R) →
    sum-finite-Commutative-Semiring R A f ＝
    sum-finite-Commutative-Semiring R A (f ∘ map-equiv σ)
  sum-aut-finite-Commutative-Semiring =
    sum-equiv-finite-Commutative-Semiring R A A (inv-equiv σ)

Sums over finite types distribute over coproducts

module _
  {l1 l2 l3 : Level} (R : Commutative-Semiring l1)
  (A : Finite-Type l2) (B : Finite-Type l3)
  where

  distributive-sum-coproduct-finite-Commutative-Semiring :
    (f :
      type-Finite-Type A + type-Finite-Type B → type-Commutative-Semiring R) →
    sum-finite-Commutative-Semiring R (coproduct-Finite-Type A B) f ＝
    add-Commutative-Semiring
      ( R)
      ( sum-finite-Commutative-Semiring R A (f ∘ inl))
      ( sum-finite-Commutative-Semiring R B (f ∘ inr))
  distributive-sum-coproduct-finite-Commutative-Semiring =
    distributive-sum-coproduct-finite-Semiring
      ( semiring-Commutative-Semiring R)
      ( A)
      ( B)

Sums distribute over dependent pair types

module _
  {l1 l2 l3 : Level} (R : Commutative-Semiring l1)
  (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3)
  where

  sum-Σ-finite-Commutative-Semiring :
    (f :
      (a : type-Finite-Type A) →
      type-Finite-Type (B a) →
      type-Commutative-Semiring R) →
    sum-finite-Commutative-Semiring R (Σ-Finite-Type A B) (ind-Σ f) ＝
    sum-finite-Commutative-Semiring
      R A (λ a → sum-finite-Commutative-Semiring R (B a) (f a))
  sum-Σ-finite-Commutative-Semiring =
    sum-Σ-finite-Semiring (semiring-Commutative-Semiring R) A B

The sum over an empty type is zero

module _
  {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2)
  (H : is-empty (type-Finite-Type A))
  where

  eq-zero-sum-finite-is-empty-Commutative-Semiring :
    (f : type-Finite-Type A → type-Commutative-Semiring R) →
    is-zero-Commutative-Semiring R (sum-finite-Commutative-Semiring R A f)
  eq-zero-sum-finite-is-empty-Commutative-Semiring =
    eq-zero-sum-finite-is-empty-Semiring (semiring-Commutative-Semiring R) A H

The sum over a finite type is the sum over any count for that type

eq-sum-finite-sum-count-Commutative-Semiring :
  {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2)
  (cA : count (type-Finite-Type A))
  (f : type-Finite-Type A → type-Commutative-Semiring R) →
  sum-finite-Commutative-Semiring R A f ＝
  sum-count-Commutative-Semiring R (type-Finite-Type A) cA f
eq-sum-finite-sum-count-Commutative-Semiring R =
  eq-sum-finite-sum-count-Semiring (semiring-Commutative-Semiring R)

Interchange law of sums and addition

module _
  {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2)
  where

  interchange-sum-add-finite-Commutative-Semiring :
    (f g : type-Finite-Type A → type-Commutative-Semiring R) →
    sum-finite-Commutative-Semiring R A
      (λ a → add-Commutative-Semiring R (f a) (g a)) ＝
    add-Commutative-Semiring R
      (sum-finite-Commutative-Semiring R A f)
      (sum-finite-Commutative-Semiring R A g)
  interchange-sum-add-finite-Commutative-Semiring =
    interchange-sum-add-finite-Semiring (semiring-Commutative-Semiring R) A

A sum of zeroes is zero

module _
  {l : Level} (R : Commutative-Semiring l)
  where

  sum-zero-finite-Commutative-Semiring :
    {l2 : Level} (A : Finite-Type l2) →
    sum-finite-Commutative-Semiring R A (λ _ → zero-Commutative-Semiring R) ＝
    zero-Commutative-Semiring R
  sum-zero-finite-Commutative-Semiring =
    sum-zero-finite-Semiring (semiring-Commutative-Semiring R)
  • Sum at Wikidata

Recent changes