Sums of finite families of elements in semirings
Content created by Louis Wasserman.
Created on 2025-06-03.
Last modified on 2025-06-03.
module ring-theory.sums-of-finite-families-of-elements-semirings where
Imports
open import foundation.action-on-identifications-functions 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.propositional-truncations open import foundation.sets open import foundation.type-arithmetic-cartesian-product-types open import foundation.unit-type open import foundation.universe-levels open import group-theory.sums-of-finite-families-of-elements-commutative-monoids open import ring-theory.semirings open import ring-theory.sums-of-finite-sequences-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 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
finite type.
Definition
sum-count-Semiring : {l1 l2 : Level} (R : Semiring l1) (A : UU l2) (cA : count A) → (A → type-Semiring R) → type-Semiring R sum-count-Semiring R = sum-count-Commutative-Monoid (additive-commutative-monoid-Semiring R) sum-finite-Semiring : {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) → (type-Finite-Type A → type-Semiring R) → type-Semiring R sum-finite-Semiring R = sum-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R)
Properties
Sums over the unit type
module _ {l : Level} (R : Semiring l) where sum-unit-finite-Semiring : (f : unit → type-Semiring R) → sum-finite-Semiring R unit-Finite-Type f = f star sum-unit-finite-Semiring = sum-finite-unit-type-Commutative-Monoid ( additive-commutative-monoid-Semiring R)
Sums are homotopy invariant
module _ {l : Level} (R : Semiring l) where htpy-sum-finite-Semiring : {l2 : Level} (A : Finite-Type l2) → {f g : type-Finite-Type A → type-Semiring R} → (f ~ g) → sum-finite-Semiring R A f = sum-finite-Semiring R A g htpy-sum-finite-Semiring = htpy-sum-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R)
Multiplication distributes over sums
module _ {l : Level} (R : Semiring l) where abstract left-distributive-mul-sum-finite-Semiring : {l2 : Level} (A : Finite-Type l2) (x : type-Semiring R) → (f : type-Finite-Type A → type-Semiring R) → mul-Semiring R x (sum-finite-Semiring R A f) = sum-finite-Semiring R A (mul-Semiring R x ∘ f) left-distributive-mul-sum-finite-Semiring A x f = let open do-syntax-trunc-Prop ( Id-Prop ( set-Semiring R) ( mul-Semiring R x (sum-finite-Semiring R A f)) ( sum-finite-Semiring R A (mul-Semiring R x ∘ f))) in do cA ← is-finite-type-Finite-Type A equational-reasoning mul-Semiring R x (sum-finite-Semiring R A f) = mul-Semiring ( R) ( x) ( sum-count-Semiring ( R) ( type-Finite-Type A) ( cA) ( f)) by ap ( mul-Semiring R x) ( eq-sum-finite-sum-count-Commutative-Monoid _ A cA f) = sum-count-Semiring R (type-Finite-Type A) cA (mul-Semiring R x ∘ f) by left-distributive-mul-sum-fin-sequence-type-Semiring ( R) ( number-of-elements-count cA) ( x) ( f ∘ map-equiv-count cA) = sum-finite-Semiring R A (mul-Semiring R x ∘ f) by inv (eq-sum-finite-sum-count-Commutative-Monoid _ A cA _) right-distributive-mul-sum-finite-Semiring : {l2 : Level} (A : Finite-Type l2) → (f : type-Finite-Type A → type-Semiring R) (x : type-Semiring R) → mul-Semiring R (sum-finite-Semiring R A f) x = sum-finite-Semiring R A (mul-Semiring' R x ∘ f) right-distributive-mul-sum-finite-Semiring A f x = let open do-syntax-trunc-Prop ( Id-Prop ( set-Semiring R) ( mul-Semiring R (sum-finite-Semiring R A f) x) ( sum-finite-Semiring R A (mul-Semiring' R x ∘ f))) in do cA ← is-finite-type-Finite-Type A equational-reasoning mul-Semiring R (sum-finite-Semiring R A f) x = mul-Semiring ( R) ( sum-count-Semiring R (type-Finite-Type A) cA f) ( x) by ap ( mul-Semiring' R x) ( eq-sum-finite-sum-count-Commutative-Monoid _ A cA f) = sum-count-Semiring R (type-Finite-Type A) cA (mul-Semiring' R x ∘ f) by right-distributive-mul-sum-fin-sequence-type-Semiring ( R) ( number-of-elements-count cA) ( f ∘ map-equiv-count cA) ( x) = sum-finite-Semiring R A (mul-Semiring' R x ∘ f) by inv (eq-sum-finite-sum-count-Commutative-Monoid _ A cA _)
A sum of zeroes is zero
module _ {l : Level} (R : Semiring l) where eq-zero-sum-zero-fin-sequence-type-RingSemiring : {l2 : Level} (A : Finite-Type l2) → sum-finite-Semiring R A (λ _ → zero-Semiring R) = zero-Semiring R eq-zero-sum-zero-fin-sequence-type-RingSemiring = eq-zero-eq-zero-sum-zero-fin-sequence-type-RingCommutative-Monoid ( additive-commutative-monoid-Semiring R)
Sums over finite types are preserved by equivalences
module _ {l1 l2 l3 : Level} (R : Semiring l1) (A : Finite-Type l2) (B : Finite-Type l3) (H : equiv-Finite-Type A B) where sum-equiv-finite-Semiring : (f : type-Finite-Type A → type-Semiring R) → sum-finite-Semiring R A f = sum-finite-Semiring R B (f ∘ map-inv-equiv H) sum-equiv-finite-Semiring = sum-equiv-finite-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( A) ( B) ( H)
Sums over finite types distribute over coproducts
module _ {l1 l2 l3 : Level} (R : Semiring l1) (A : Finite-Type l2) (B : Finite-Type l3) where distributive-sum-coproduct-finite-Semiring : (f : type-Finite-Type A + type-Finite-Type B → type-Semiring R) → sum-finite-Semiring R (coproduct-Finite-Type A B) f = add-Semiring ( R) ( sum-finite-Semiring R A (f ∘ inl)) ( sum-finite-Semiring R B (f ∘ inr)) distributive-sum-coproduct-finite-Semiring = distributive-distributive-sum-coproduct-finite-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( A) ( B)
Sums distribute over dependent pair types
module _ {l1 l2 l3 : Level} (R : Semiring l1) (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) where sum-Σ-finite-Semiring : (f : (a : type-Finite-Type A) → type-Finite-Type (B a) → type-Semiring R) → sum-finite-Semiring R (Σ-Finite-Type A B) (ind-Σ f) = sum-finite-Semiring R A (λ a → sum-finite-Semiring R (B a) (f a)) sum-Σ-finite-Semiring = sum-Σ-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R) A B
The sum over an empty type is zero
module _ {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) (H : is-empty (type-Finite-Type A)) where eq-zero-sum-finite-is-empty-Semiring : (f : type-Finite-Type A → type-Semiring R) → is-zero-Semiring R (sum-finite-Semiring R A f) eq-zero-sum-finite-is-empty-Semiring = eq-zero-sum-finite-is-empty-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( A) ( H)
The sum over a finite type is the sum over any count for that type
eq-sum-finite-sum-count-Semiring : {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) (cA : count (type-Finite-Type A)) (f : type-Finite-Type A → type-Semiring R) → sum-finite-Semiring R A f = sum-count-Semiring R (type-Finite-Type A) cA f eq-sum-finite-sum-count-Semiring R = eq-sum-finite-sum-count-Commutative-Monoid ( additive-commutative-monoid-Semiring R)
Interchange law of sums and addition
module _ {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) where interchange-sum-add-finite-Semiring : (f g : type-Finite-Type A → type-Semiring R) → sum-finite-Semiring R A (λ a → add-Semiring R (f a) (g a)) = add-Semiring R (sum-finite-Semiring R A f) (sum-finite-Semiring R A g) interchange-sum-add-finite-Semiring f g = equational-reasoning sum-finite-Semiring R A ( λ a → add-Semiring R (f a) (g a)) = sum-finite-Semiring ( R) ( A) ( λ a → sum-fin-sequence-type-Semiring R 2 (h a)) by htpy-sum-finite-Semiring ( R) ( A) ( λ a → inv (compute-sum-two-elements-Semiring R (h a))) = sum-finite-Semiring ( R) ( A) ( λ a → sum-finite-Semiring R (Fin-Finite-Type 2) (h a)) by htpy-sum-finite-Semiring R A ( λ a → inv ( eq-sum-finite-sum-count-Semiring ( R) ( Fin-Finite-Type 2) ( count-Fin 2) ( h a))) = sum-finite-Semiring ( R) ( Σ-Finite-Type A (λ _ → Fin-Finite-Type 2)) ( ind-Σ h) by inv (sum-Σ-finite-Semiring R A (λ _ → Fin-Finite-Type 2) h) = sum-finite-Semiring ( R) ( Σ-Finite-Type (Fin-Finite-Type 2) (λ _ → A)) ( λ (i , a) → h a i) by sum-equiv-finite-Semiring R _ _ ( commutative-product) ( ind-Σ h) = sum-finite-Semiring ( R) ( Fin-Finite-Type 2) ( λ i → sum-finite-Semiring R A (λ a → h a i)) by sum-Σ-finite-Semiring R _ _ _ = sum-fin-sequence-type-Semiring ( R) ( 2) ( λ i → sum-finite-Semiring R A (λ a → h a i)) by eq-sum-finite-sum-count-Semiring ( R) ( Fin-Finite-Type 2) ( count-Fin 2) ( _) = add-Semiring ( R) ( sum-finite-Semiring R A f) ( sum-finite-Semiring R A g) by compute-sum-two-elements-Semiring ( R) ( λ i → sum-finite-Semiring R A (λ a → h a i)) where h : type-Finite-Type A → Fin 2 → type-Semiring R h a (inl (inr _)) = f a h a (inr _) = g a
External links
- Sum at Wikidata
Recent changes
- 2025-06-03. Louis Wasserman. Sums and products over arbitrary finite types (#1367).