Sums of finite sequences 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-sequences-of-elements-commutative-rings where
Imports 
open import commutative-algebra.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.coproduct-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.finite-sequences-in-commutative-rings

open import lists.finite-sequences

open import ring-theory.sums-of-finite-sequences-of-elements-rings

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

Idea

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

Definition

sum-fin-sequence-type-Commutative-Ring :
  {l : Level} (A : Commutative-Ring l) (n : ℕ) →
  (fin-sequence-type-Commutative-Ring A n) → type-Commutative-Ring A
sum-fin-sequence-type-Commutative-Ring A =
  sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

Properties

Sums of one and two elements

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

  compute-sum-one-element-Commutative-Ring :
    (f : fin-sequence-type-Commutative-Ring A 1) →
    sum-fin-sequence-type-Commutative-Ring A 1 f ＝ head-fin-sequence 0 f
  compute-sum-one-element-Commutative-Ring =
    compute-sum-one-element-Ring (ring-Commutative-Ring A)

  compute-sum-two-elements-Commutative-Ring :
    (f : fin-sequence-type-Commutative-Ring A 2) →
    sum-fin-sequence-type-Commutative-Ring A 2 f ＝
    add-Commutative-Ring A (f (zero-Fin 1)) (f (one-Fin 1))
  compute-sum-two-elements-Commutative-Ring =
    compute-sum-two-elements-Ring (ring-Commutative-Ring A)

Sums are homotopy invariant

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

  htpy-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) {f g : fin-sequence-type-Commutative-Ring R n} →
    (f ~ g) →
    sum-fin-sequence-type-Commutative-Ring R n f ＝
    sum-fin-sequence-type-Commutative-Ring R n g
  htpy-sum-fin-sequence-type-Commutative-Ring =
    htpy-sum-fin-sequence-type-Ring (ring-Commutative-Ring R)

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

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

  cons-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (f : fin-sequence-type-Commutative-Ring A (succ-ℕ n)) →
    {x : type-Commutative-Ring A} → head-fin-sequence n f ＝ x →
    sum-fin-sequence-type-Commutative-Ring A (succ-ℕ n) f ＝
    add-Commutative-Ring A
      ( sum-fin-sequence-type-Commutative-Ring A n (tail-fin-sequence n f)) x
  cons-sum-fin-sequence-type-Commutative-Ring =
    cons-sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

  snoc-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (f : fin-sequence-type-Commutative-Ring A (succ-ℕ n)) →
    {x : type-Commutative-Ring A} → f (zero-Fin n) ＝ x →
    sum-fin-sequence-type-Commutative-Ring A (succ-ℕ n) f ＝
    add-Commutative-Ring A
      ( x)
      ( sum-fin-sequence-type-Commutative-Ring A n (f ∘ inr-Fin n))
  snoc-sum-fin-sequence-type-Commutative-Ring =
    snoc-sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

Multiplication distributes over sums

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

  left-distributive-mul-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (x : type-Commutative-Ring R)
    (f : fin-sequence-type-Commutative-Ring R n) →
    mul-Commutative-Ring R x (sum-fin-sequence-type-Commutative-Ring R n f) ＝
    sum-fin-sequence-type-Commutative-Ring R n (mul-Commutative-Ring R x ∘ f)
  left-distributive-mul-sum-fin-sequence-type-Commutative-Ring =
    left-distributive-mul-sum-fin-sequence-type-Ring (ring-Commutative-Ring R)

  right-distributive-mul-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (f : fin-sequence-type-Commutative-Ring R n)
    (x : type-Commutative-Ring R) →
    mul-Commutative-Ring R (sum-fin-sequence-type-Commutative-Ring R n f) x ＝
    sum-fin-sequence-type-Commutative-Ring R n (mul-Commutative-Ring' R x ∘ f)
  right-distributive-mul-sum-fin-sequence-type-Commutative-Ring =
    right-distributive-mul-sum-fin-sequence-type-Ring (ring-Commutative-Ring R)

Interchange law of sums and addition in a commutative ring

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

  interchange-add-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (f g : fin-sequence-type-Commutative-Ring A n) →
    add-Commutative-Ring A
      ( sum-fin-sequence-type-Commutative-Ring A n f)
      ( sum-fin-sequence-type-Commutative-Ring A n g) ＝
    sum-fin-sequence-type-Commutative-Ring A n
      ( add-fin-sequence-type-Commutative-Ring A n f g)
  interchange-add-sum-fin-sequence-type-Commutative-Ring =
    interchange-add-sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

Extending a sum of elements in a commutative ring

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

  extend-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (f : fin-sequence-type-Commutative-Ring A n) →
    sum-fin-sequence-type-Commutative-Ring A
      ( succ-ℕ n)
      ( cons-fin-sequence-type-Commutative-Ring
        ( A)
        ( n)
        ( zero-Commutative-Ring A)
        ( f)) ＝
    sum-fin-sequence-type-Commutative-Ring A n f
  extend-sum-fin-sequence-type-Commutative-Ring =
    extend-sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

Shifting a sum of elements in a commutative ring

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

  shift-sum-fin-sequence-type-Commutative-Ring :
    (n : ℕ) (f : fin-sequence-type-Commutative-Ring A n) →
    sum-fin-sequence-type-Commutative-Ring A
      ( succ-ℕ n)
      ( snoc-fin-sequence-type-Commutative-Ring A n f
        ( zero-Commutative-Ring A)) ＝
    sum-fin-sequence-type-Commutative-Ring A n f
  shift-sum-fin-sequence-type-Commutative-Ring =
    shift-sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

Splitting sums of n + m elements into a sum of n elements and a sum of m elements

split-sum-fin-sequence-type-Commutative-Ring :
  {l : Level} (A : Commutative-Ring l)
  (n m : ℕ) (f : fin-sequence-type-Commutative-Ring A (n +ℕ m)) →
  sum-fin-sequence-type-Commutative-Ring A (n +ℕ m) f ＝
  add-Commutative-Ring A
    ( sum-fin-sequence-type-Commutative-Ring A n (f ∘ inl-coproduct-Fin n m))
    ( sum-fin-sequence-type-Commutative-Ring A m (f ∘ inr-coproduct-Fin n m))
split-sum-fin-sequence-type-Commutative-Ring A =
  split-sum-fin-sequence-type-Ring (ring-Commutative-Ring A)

A sum of zeroes is zero

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

  sum-zero-fin-sequence-type-Commutative-Ring :
    (n : ℕ) →
    sum-fin-sequence-type-Commutative-Ring R n
      ( zero-fin-sequence-type-Commutative-Ring R n) ＝
    zero-Commutative-Ring R
  sum-zero-fin-sequence-type-Commutative-Ring =
    sum-zero-fin-sequence-type-Ring (ring-Commutative-Ring R)

Permutations preserve sums

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

  preserves-sum-permutation-fin-sequence-type-Commutative-Ring :
    (n : ℕ) → (σ : Permutation n) →
    (f : fin-sequence-type-Commutative-Ring A n) →
    sum-fin-sequence-type-Commutative-Ring A n f ＝
    sum-fin-sequence-type-Commutative-Ring A n (f ∘ map-equiv σ)
  preserves-sum-permutation-fin-sequence-type-Commutative-Ring =
    preserves-sum-permutation-fin-sequence-type-Ring (ring-Commutative-Ring A)

See also

  • Sum at Wikidata

Recent changes