Sums of finite families in commutative rings

Content created by Louis Wasserman.

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

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

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-rings

open import ring-theory.sums-of-finite-families-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 commutative ring A to any family of elements of A indexed by a finite type.

Definition

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

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

Properties

Sums over the unit types

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

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

Sums are homotopy invariant

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

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

Multiplication distributes over sums

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

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

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

Sums over finite types are preserved by equivalences

sum-equiv-finite-Commutative-Ring :
  {l1 l2 l3 : Level} (R : Commutative-Ring l1) →
  (A : Finite-Type l2) (B : Finite-Type l3) (H : equiv-Finite-Type A B) →
  (f : type-Finite-Type A → type-Commutative-Ring R) →
  sum-finite-Commutative-Ring R A f ＝
  sum-finite-Commutative-Ring R B (f ∘ map-inv-equiv H)
sum-equiv-finite-Commutative-Ring R =
  sum-equiv-finite-Commutative-Semiring
    ( commutative-semiring-Commutative-Ring R)

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

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

Sums over finite types distribute over coproducts

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

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

Sums distribute over dependent pair types

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

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

The sum over an empty type is zero

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

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

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

eq-sum-finite-sum-count-Commutative-Ring :
  {l1 l2 : Level} (R : Commutative-Ring l1) (A : Finite-Type l2)
  (cA : count (type-Finite-Type A))
  (f : type-Finite-Type A → type-Commutative-Ring R) →
  sum-finite-Commutative-Ring R A f ＝
  sum-count-Commutative-Ring R (type-Finite-Type A) cA f
eq-sum-finite-sum-count-Commutative-Ring R =
  eq-sum-finite-sum-count-Ring (ring-Commutative-Ring R)
  • Sum at Wikidata

Recent changes