Sums of elements in semirings

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Maša Žaucer.

Created on 2023-02-20.

module ring-theory.sums-semirings 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 linear-algebra.vectors
open import linear-algebra.vectors-on-semirings

open import ring-theory.semirings

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


Idea

The sum operation extends the binary addition operation on a semiring R to any family of elements of R indexed by a standard finite type.

Definition

sum-Semiring :
{l : Level} (R : Semiring l) (n : ℕ) →
(functional-vec-Semiring R n) → type-Semiring R
sum-Semiring R zero-ℕ f = zero-Semiring R
sum-Semiring R (succ-ℕ n) f =
( sum-Semiring R n (f ∘ inl-Fin n))
( f (inr star))


Properties

Sums of one and two elements

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

sum-one-element-Semiring :
(f : functional-vec-Semiring R 1) →
sum-Semiring R 1 f ＝ head-functional-vec 0 f
sum-one-element-Semiring f =

sum-two-elements-Semiring :
(f : functional-vec-Semiring R 2) →
sum-Semiring R 2 f ＝ add-Semiring R (f (zero-Fin 1)) (f (one-Fin 1))
sum-two-elements-Semiring f =
(zero-Semiring R) (f (zero-Fin 1)) (f (one-Fin 1))) ∙
( add-Semiring R (f (zero-Fin 1)) (f (one-Fin 1))))


Sums are homotopy invariant

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

htpy-sum-Semiring :
(n : ℕ) {f g : functional-vec-Semiring R n} →
(f ~ g) → sum-Semiring R n f ＝ sum-Semiring R n g
htpy-sum-Semiring zero-ℕ H = refl
htpy-sum-Semiring (succ-ℕ n) H =
( htpy-sum-Semiring n (H ·r inl-Fin n))
( H (inr star))


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

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

cons-sum-Semiring :
(n : ℕ) (f : functional-vec-Semiring R (succ-ℕ n)) →
{x : type-Semiring R} → head-functional-vec n f ＝ x →
sum-Semiring R (succ-ℕ n) f ＝
add-Semiring R (sum-Semiring R n (f ∘ inl-Fin n)) x
cons-sum-Semiring n f refl = refl

snoc-sum-Semiring :
(n : ℕ) (f : functional-vec-Semiring R (succ-ℕ n)) →
{x : type-Semiring R} → f (zero-Fin n) ＝ x →
sum-Semiring R (succ-ℕ n) f ＝
( x)
( sum-Semiring R n (f ∘ inr-Fin n))
snoc-sum-Semiring zero-ℕ f refl =
( sum-one-element-Semiring R f) ∙
( inv (right-unit-law-add-Semiring R (f (zero-Fin 0))))
snoc-sum-Semiring (succ-ℕ n) f refl =
( ap
( snoc-sum-Semiring n (f ∘ inl-Fin (succ-ℕ n)) refl)) ∙
( f (zero-Fin (succ-ℕ n)))
( sum-Semiring R n (f ∘ (inr-Fin (succ-ℕ n) ∘ inl-Fin n)))


Multiplication distributes over sums

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

left-distributive-mul-sum-Semiring :
(n : ℕ) (x : type-Semiring R)
(f : functional-vec-Semiring R n) →
mul-Semiring R x (sum-Semiring R n f) ＝
sum-Semiring R n (λ i → mul-Semiring R x (f i))
left-distributive-mul-sum-Semiring zero-ℕ x f =
right-zero-law-mul-Semiring R x
left-distributive-mul-sum-Semiring (succ-ℕ n) x f =
( sum-Semiring R n (f ∘ inl-Fin n))
( f (inr star))) ∙
( ap
( add-Semiring' R (mul-Semiring R x (f (inr star))))
( left-distributive-mul-sum-Semiring n x (f ∘ inl-Fin n)))

right-distributive-mul-sum-Semiring :
(n : ℕ) (f : functional-vec-Semiring R n)
(x : type-Semiring R) →
mul-Semiring R (sum-Semiring R n f) x ＝
sum-Semiring R n (λ i → mul-Semiring R (f i) x)
right-distributive-mul-sum-Semiring zero-ℕ f x =
left-zero-law-mul-Semiring R x
right-distributive-mul-sum-Semiring (succ-ℕ n) f x =
( sum-Semiring R n (f ∘ inl-Fin n))
( f (inr star))
( x)) ∙
( ap
( add-Semiring' R (mul-Semiring R (f (inr star)) x))
( right-distributive-mul-sum-Semiring n (f ∘ inl-Fin n) x))


Interchange law of sums and addition in a semiring

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

(n : ℕ) (f g : functional-vec-Semiring R n) →
( sum-Semiring R n f)
( sum-Semiring R n g) ＝
sum-Semiring R n
( add-functional-vec-Semiring R n f g)
interchange-add-sum-Semiring (succ-ℕ n) f g =
( sum-Semiring R n (f ∘ inl-Fin n))
( f (inr star))
( sum-Semiring R n (g ∘ inl-Fin n))
( g (inr star))) ∙
( ap
( add-Semiring R (f (inr star)) (g (inr star))))
( f ∘ inl-Fin n)
( g ∘ inl-Fin n)))


Extending a sum of elements in a semiring

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

extend-sum-Semiring :
(n : ℕ) (f : functional-vec-Semiring R n) →
sum-Semiring R
( succ-ℕ n)
( cons-functional-vec-Semiring R n (zero-Semiring R) f) ＝
sum-Semiring R n f
extend-sum-Semiring n f =
right-unit-law-add-Semiring R (sum-Semiring R n f)


Shifting a sum of elements in a semiring

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

shift-sum-Semiring :
(n : ℕ) (f : functional-vec-Semiring R n) →
sum-Semiring R
( succ-ℕ n)
( snoc-functional-vec-Semiring R n f
( zero-Semiring R)) ＝
sum-Semiring R n f
shift-sum-Semiring zero-ℕ f =
shift-sum-Semiring (succ-ℕ n) f =
ap
( shift-sum-Semiring n
( tail-functional-vec-Semiring R n f))


A sum of zeroes is zero

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

sum-zero-Semiring :
(n : ℕ) →
sum-Semiring R n (zero-functional-vec-Semiring R n) ＝ zero-Semiring R
sum-zero-Semiring zero-ℕ = refl
sum-zero-Semiring (succ-ℕ n) =
right-unit-law-add-Semiring R _ ∙ sum-zero-Semiring n


Splitting sums

split-sum-Semiring :
{l : Level} (R : Semiring l)
(n m : ℕ) (f : functional-vec-Semiring R (n +ℕ m)) →
sum-Semiring R (n +ℕ m) f ＝