Sums of finite families of elements in rings
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-rings where
Imports
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 ring-theory.rings open import ring-theory.sums-of-finite-families-of-elements-semirings open import ring-theory.sums-of-finite-sequences-of-elements-rings 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 ring R
to
any family of elements of R
indexed by a
finite type
Definition
sum-count-Ring : {l1 l2 : Level} (R : Ring l1) (A : UU l2) → count A → (A → type-Ring R) → type-Ring R sum-count-Ring R = sum-count-Semiring (semiring-Ring R) sum-finite-Ring : {l1 l2 : Level} (R : Ring l1) (A : Finite-Type l2) → (type-Finite-Type A → type-Ring R) → type-Ring R sum-finite-Ring R = sum-finite-Semiring (semiring-Ring R)
Properties
Sums over the unit type
module _ {l : Level} (R : Ring l) where sum-unit-finite-Ring : (f : unit → type-Ring R) → sum-finite-Ring R unit-Finite-Type f = f star sum-unit-finite-Ring = sum-unit-finite-Semiring (semiring-Ring R)
Sums are homotopy invariant
module _ {l : Level} (R : Ring l) where htpy-sum-finite-Ring : {l2 : Level} (A : Finite-Type l2) → {f g : type-Finite-Type A → type-Ring R} → (f ~ g) → sum-finite-Ring R A f = sum-finite-Ring R A g htpy-sum-finite-Ring = htpy-sum-finite-Semiring (semiring-Ring R)
Multiplication distributes over sums
module _ {l : Level} (R : Ring l) where left-distributive-mul-sum-finite-Ring : {l2 : Level} (A : Finite-Type l2) (x : type-Ring R) → (f : type-Finite-Type A → type-Ring R) → mul-Ring R x (sum-finite-Ring R A f) = sum-finite-Ring R A (mul-Ring R x ∘ f) left-distributive-mul-sum-finite-Ring = left-distributive-mul-sum-finite-Semiring (semiring-Ring R) right-distributive-mul-sum-finite-Ring : {l2 : Level} (A : Finite-Type l2) → (f : type-Finite-Type A → type-Ring R) (x : type-Ring R) → mul-Ring R (sum-finite-Ring R A f) x = sum-finite-Ring R A (mul-Ring' R x ∘ f) right-distributive-mul-sum-finite-Ring = right-distributive-mul-sum-finite-Semiring (semiring-Ring R)
A sum of zeroes is zero
module _ {l : Level} (R : Ring l) where eq-zero-sum-zero-fin-sequence-type-RingRing : {l2 : Level} (A : Finite-Type l2) → sum-finite-Ring R A (λ _ → zero-Ring R) = zero-Ring R eq-zero-sum-zero-fin-sequence-type-RingRing = eq-zero-sum-zero-fin-sequence-type-RingSemiring (semiring-Ring R)
Sums over finite types are preserved by equivalences
module _ {l1 l2 l3 : Level} (R : Ring l1) (A : Finite-Type l2) (B : Finite-Type l3) (H : equiv-Finite-Type A B) where sum-equiv-finite-Ring : (f : type-Finite-Type A → type-Ring R) → sum-finite-Ring R A f = sum-finite-Ring R B (f ∘ map-inv-equiv H) sum-equiv-finite-Ring = sum-equiv-finite-Semiring (semiring-Ring R) A B H
Sums over finite types distribute over coproducts
module _ {l1 l2 l3 : Level} (R : Ring l1) (A : Finite-Type l2) (B : Finite-Type l3) where distributive-sum-coproduct-finite-Ring : (f : type-Finite-Type A + type-Finite-Type B → type-Ring R) → sum-finite-Ring R (coproduct-Finite-Type A B) f = add-Ring ( R) ( sum-finite-Ring R A (f ∘ inl)) ( sum-finite-Ring R B (f ∘ inr)) distributive-sum-coproduct-finite-Ring = distributive-sum-coproduct-finite-Semiring (semiring-Ring R) A B
Sums distribute over dependent pair types
module _ {l1 l2 l3 : Level} (R : Ring l1) (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) where sum-Σ-finite-Ring : (f : (a : type-Finite-Type A) → type-Finite-Type (B a) → type-Ring R) → sum-finite-Ring R (Σ-Finite-Type A B) (ind-Σ f) = sum-finite-Ring R A (λ a → sum-finite-Ring R (B a) (f a)) sum-Σ-finite-Ring = sum-Σ-finite-Semiring (semiring-Ring R) A B
The sum over an empty type is zero
module _ {l1 l2 : Level} (R : Ring l1) (A : Finite-Type l2) (H : is-empty (type-Finite-Type A)) where eq-zero-sum-finite-is-empty-Ring : (f : type-Finite-Type A → type-Ring R) → is-zero-Ring R (sum-finite-Ring R A f) eq-zero-sum-finite-is-empty-Ring = eq-zero-sum-finite-is-empty-Semiring (semiring-Ring R) A H
The sum over a finite type is the sum over any count for that type
eq-sum-finite-sum-count-Ring : {l1 l2 : Level} (R : Ring l1) (A : Finite-Type l2) (cA : count (type-Finite-Type A)) (f : type-Finite-Type A → type-Ring R) → sum-finite-Ring R A f = sum-count-Ring R (type-Finite-Type A) cA f eq-sum-finite-sum-count-Ring R = eq-sum-finite-sum-count-Semiring (semiring-Ring R)
External links
- Sum at Wikidata
Recent changes
- 2025-06-03. Louis Wasserman. Sums and products over arbitrary finite types (#1367).