Formal power series in commutative semirings

Content created by Louis Wasserman.

Created on 2025-09-09.
Last modified on 2025-09-11.

module commutative-algebra.formal-power-series-commutative-semirings where
Imports 
open import commutative-algebra.commutative-semirings
open import commutative-algebra.convolution-sequences-commutative-semirings
open import commutative-algebra.function-commutative-semirings
open import commutative-algebra.homomorphisms-commutative-semirings
open import commutative-algebra.powers-of-elements-commutative-semirings
open import commutative-algebra.sums-of-finite-families-of-elements-commutative-semirings

open import elementary-number-theory.binary-sum-decompositions-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.homomorphisms-commutative-monoids
open import group-theory.monoids
open import group-theory.semigroups

open import lists.sequences

open import ring-theory.semirings

Idea

A formal power series is a formal sum of the form Σₙ aₙxⁿ, without any notion of convergence.

Definition

Formal power series are defined with a record to make them intensionally distinct from the sequence of their coefficients.

record
  formal-power-series-Commutative-Semiring
    {l : Level} (R : Commutative-Semiring l) : UU l
  where

  constructor formal-power-series-coefficients-Commutative-Semiring

  field
    coefficient-formal-power-series-Commutative-Semiring :
      sequence (type-Commutative-Semiring R)

open formal-power-series-Commutative-Semiring public

Properties

The terms in the infinite sum of evaluating a formal power series at an argument

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  term-ev-formal-power-series-Commutative-Semiring :
    (f : formal-power-series-Commutative-Semiring R) →
    (x : type-Commutative-Semiring R) →
    sequence (type-Commutative-Semiring R)
  term-ev-formal-power-series-Commutative-Semiring
    ( formal-power-series-coefficients-Commutative-Semiring a)
    ( x)
    ( n) =
    mul-Commutative-Semiring R (a n) (power-Commutative-Semiring R n x)

Equivalence to sequences in the commutative semiring

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

  equiv-formal-power-series-sequence-Commutative-Semiring :
    sequence (type-Commutative-Semiring R) ≃
    formal-power-series-Commutative-Semiring R
  equiv-formal-power-series-sequence-Commutative-Semiring =
    ( formal-power-series-coefficients-Commutative-Semiring ,
      is-equiv-is-invertible
        ( coefficient-formal-power-series-Commutative-Semiring)
        ( λ _ → refl)
        ( λ _ → refl))

The set of formal power series

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

  abstract
    is-set-formal-power-series-Commutative-Semiring :
      is-set (formal-power-series-Commutative-Semiring R)
    is-set-formal-power-series-Commutative-Semiring =
      is-set-equiv
        ( _)
        ( inv-equiv (equiv-formal-power-series-sequence-Commutative-Semiring R))
        ( is-set-type-Π-Set' _ (λ _ → set-Commutative-Semiring R))

  set-formal-power-series-Commutative-Semiring : Set l
  set-formal-power-series-Commutative-Semiring =
    ( formal-power-series-Commutative-Semiring R ,
      is-set-formal-power-series-Commutative-Semiring)

The constant zero formal power series

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

  zero-formal-power-series-Commutative-Semiring :
    formal-power-series-Commutative-Semiring R
  zero-formal-power-series-Commutative-Semiring =
    formal-power-series-coefficients-Commutative-Semiring
      ( zero-Commutative-Semiring
        ( commutative-semiring-convolution-sequence-Commutative-Semiring R))

The constant one formal power series

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

  one-formal-power-series-Commutative-Semiring :
    formal-power-series-Commutative-Semiring R
  one-formal-power-series-Commutative-Semiring =
    formal-power-series-coefficients-Commutative-Semiring
      ( one-Commutative-Semiring
        ( commutative-semiring-convolution-sequence-Commutative-Semiring R))

The identity formal power series

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

  id-formal-power-series-Commutative-Semiring :
    formal-power-series-Commutative-Semiring R
  id-formal-power-series-Commutative-Semiring =
    formal-power-series-coefficients-Commutative-Semiring
      ( λ where
          zero-ℕ → zero-Commutative-Semiring R
          (succ-ℕ zero-ℕ) → one-Commutative-Semiring R
          (succ-ℕ (succ-ℕ _)) → zero-Commutative-Semiring R)

Constant formal power series

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

  constant-formal-power-series-Commutative-Semiring :
    type-Commutative-Semiring R → formal-power-series-Commutative-Semiring R
  constant-formal-power-series-Commutative-Semiring c =
    formal-power-series-coefficients-Commutative-Semiring
      ( λ where
        zero-ℕ → c
        (succ-ℕ _) → zero-Commutative-Semiring R)

The constant zero formal power series is the constant formal power series with value zero

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

  abstract
    constant-zero-formal-power-series-Commutative-Semiring :
      constant-formal-power-series-Commutative-Semiring R
        ( zero-Commutative-Semiring R) ＝
      zero-formal-power-series-Commutative-Semiring R
    constant-zero-formal-power-series-Commutative-Semiring =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( eq-htpy
          ( λ where
            zero-ℕ → refl
            (succ-ℕ _) → refl))

The constant one formal power series is the constant formal power series with value one

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

  abstract
    constant-one-formal-power-series-Commutative-Semiring :
      constant-formal-power-series-Commutative-Semiring R
        ( one-Commutative-Semiring R) ＝
      one-formal-power-series-Commutative-Semiring R
    constant-one-formal-power-series-Commutative-Semiring =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( eq-htpy
          ( λ where
            zero-ℕ → refl
            (succ-ℕ _) → refl))

Addition

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  add-formal-power-series-Commutative-Semiring :
    formal-power-series-Commutative-Semiring R →
    formal-power-series-Commutative-Semiring R →
    formal-power-series-Commutative-Semiring R
  add-formal-power-series-Commutative-Semiring x y =
    formal-power-series-coefficients-Commutative-Semiring
      ( add-Commutative-Semiring
        ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y))

Associativity

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    associative-add-formal-power-series-Commutative-Semiring :
      (x y z : formal-power-series-Commutative-Semiring R) →
      add-formal-power-series-Commutative-Semiring
        ( add-formal-power-series-Commutative-Semiring x y)
        ( z) ＝
      add-formal-power-series-Commutative-Semiring
        ( x)
        ( add-formal-power-series-Commutative-Semiring y z)
    associative-add-formal-power-series-Commutative-Semiring x y z =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( associative-add-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y)
          ( coefficient-formal-power-series-Commutative-Semiring z))

Commutativity

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    commutative-add-formal-power-series-Commutative-Semiring :
      (x y : formal-power-series-Commutative-Semiring R) →
      add-formal-power-series-Commutative-Semiring x y ＝
      add-formal-power-series-Commutative-Semiring y x
    commutative-add-formal-power-series-Commutative-Semiring x y =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( commutative-add-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y))

Unit laws

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    left-unit-law-add-formal-power-series-Commutative-Semiring :
      (x : formal-power-series-Commutative-Semiring R) →
      add-formal-power-series-Commutative-Semiring
        ( zero-formal-power-series-Commutative-Semiring R)
        ( x) ＝
      x
    left-unit-law-add-formal-power-series-Commutative-Semiring x =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( left-unit-law-add-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x))

    right-unit-law-add-formal-power-series-Commutative-Semiring :
      (x : formal-power-series-Commutative-Semiring R) →
      add-formal-power-series-Commutative-Semiring
        ( x)
        ( zero-formal-power-series-Commutative-Semiring R) ＝
      x
    right-unit-law-add-formal-power-series-Commutative-Semiring x =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( right-unit-law-add-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x))

Multiplication

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  mul-formal-power-series-Commutative-Semiring :
    formal-power-series-Commutative-Semiring R →
    formal-power-series-Commutative-Semiring R →
    formal-power-series-Commutative-Semiring R
  mul-formal-power-series-Commutative-Semiring x y =
    formal-power-series-coefficients-Commutative-Semiring
      ( mul-Commutative-Semiring
        ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y))

Associativity

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    associative-mul-formal-power-series-Commutative-Semiring :
      (x y z : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( mul-formal-power-series-Commutative-Semiring x y)
        ( z) ＝
      mul-formal-power-series-Commutative-Semiring
        ( x)
        ( mul-formal-power-series-Commutative-Semiring y z)
    associative-mul-formal-power-series-Commutative-Semiring x y z =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( associative-mul-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y)
          ( coefficient-formal-power-series-Commutative-Semiring z))

Commutativity

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    commutative-mul-formal-power-series-Commutative-Semiring :
      (x y : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring x y ＝
      mul-formal-power-series-Commutative-Semiring y x
    commutative-mul-formal-power-series-Commutative-Semiring x y =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( commutative-mul-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y))

Unit laws

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    left-unit-law-mul-formal-power-series-Commutative-Semiring :
      (x : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( one-formal-power-series-Commutative-Semiring R)
        ( x) ＝
      x
    left-unit-law-mul-formal-power-series-Commutative-Semiring x =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( left-unit-law-mul-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x))

    right-unit-law-mul-formal-power-series-Commutative-Semiring :
      (x : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( x)
        ( one-formal-power-series-Commutative-Semiring R) ＝
      x
    right-unit-law-mul-formal-power-series-Commutative-Semiring x =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( right-unit-law-mul-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x))

Zero laws

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    left-zero-law-mul-formal-power-series-Commutative-Semiring :
      (x : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( zero-formal-power-series-Commutative-Semiring R)
        ( x) ＝
      zero-formal-power-series-Commutative-Semiring R
    left-zero-law-mul-formal-power-series-Commutative-Semiring x =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( left-zero-law-mul-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x))

    right-zero-law-mul-formal-power-series-Commutative-Semiring :
      (x : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( x)
        ( zero-formal-power-series-Commutative-Semiring R) ＝
      zero-formal-power-series-Commutative-Semiring R
    right-zero-law-mul-formal-power-series-Commutative-Semiring x =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( right-zero-law-mul-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x))

Distributive laws

module _
  {l : Level} {R : Commutative-Semiring l}
  where

  abstract
    left-distributive-mul-add-formal-power-series-Commutative-Semiring :
      (x y z : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( x)
        ( add-formal-power-series-Commutative-Semiring y z) ＝
      add-formal-power-series-Commutative-Semiring
        ( mul-formal-power-series-Commutative-Semiring x y)
        ( mul-formal-power-series-Commutative-Semiring x z)
    left-distributive-mul-add-formal-power-series-Commutative-Semiring x y z =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( left-distributive-mul-add-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y)
          ( coefficient-formal-power-series-Commutative-Semiring z))

    right-distributive-mul-add-formal-power-series-Commutative-Semiring :
      (x y z : formal-power-series-Commutative-Semiring R) →
      mul-formal-power-series-Commutative-Semiring
        ( add-formal-power-series-Commutative-Semiring x y)
        ( z) ＝
      add-formal-power-series-Commutative-Semiring
        ( mul-formal-power-series-Commutative-Semiring x z)
        ( mul-formal-power-series-Commutative-Semiring y z)
    right-distributive-mul-add-formal-power-series-Commutative-Semiring x y z =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( right-distributive-mul-add-Commutative-Semiring
          ( commutative-semiring-convolution-sequence-Commutative-Semiring R)
          ( coefficient-formal-power-series-Commutative-Semiring x)
          ( coefficient-formal-power-series-Commutative-Semiring y)
          ( coefficient-formal-power-series-Commutative-Semiring z))

The commutative semiring of formal power series

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

  additive-semigroup-formal-power-series-Commutative-Semiring : Semigroup l
  additive-semigroup-formal-power-series-Commutative-Semiring =
    ( set-formal-power-series-Commutative-Semiring R ,
      add-formal-power-series-Commutative-Semiring ,
      associative-add-formal-power-series-Commutative-Semiring)

  additive-monoid-formal-power-series-Commutative-Semiring : Monoid l
  additive-monoid-formal-power-series-Commutative-Semiring =
    ( additive-semigroup-formal-power-series-Commutative-Semiring ,
      zero-formal-power-series-Commutative-Semiring R ,
      left-unit-law-add-formal-power-series-Commutative-Semiring ,
      right-unit-law-add-formal-power-series-Commutative-Semiring)

  additive-commutative-monoid-formal-power-series-Commutative-Semiring :
    Commutative-Monoid l
  additive-commutative-monoid-formal-power-series-Commutative-Semiring =
    ( additive-monoid-formal-power-series-Commutative-Semiring ,
      commutative-add-formal-power-series-Commutative-Semiring)

  semiring-formal-power-series-Commutative-Semiring : Semiring l
  semiring-formal-power-series-Commutative-Semiring =
    ( additive-commutative-monoid-formal-power-series-Commutative-Semiring ,
      ( ( mul-formal-power-series-Commutative-Semiring ,
          associative-mul-formal-power-series-Commutative-Semiring) ,
        ( one-formal-power-series-Commutative-Semiring R ,
          left-unit-law-mul-formal-power-series-Commutative-Semiring ,
          right-unit-law-mul-formal-power-series-Commutative-Semiring) ,
        left-distributive-mul-add-formal-power-series-Commutative-Semiring ,
        right-distributive-mul-add-formal-power-series-Commutative-Semiring) ,
      left-zero-law-mul-formal-power-series-Commutative-Semiring ,
      right-zero-law-mul-formal-power-series-Commutative-Semiring)

  commutative-semiring-formal-power-series-Commutative-Semiring :
    Commutative-Semiring l
  commutative-semiring-formal-power-series-Commutative-Semiring =
    ( semiring-formal-power-series-Commutative-Semiring ,
      commutative-mul-formal-power-series-Commutative-Semiring)

The constant formal power series operation is a ring homomorphism

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

  abstract
    preserves-mul-constant-formal-power-series-Commutative-Semiring :
      {x y : type-Commutative-Semiring R} →
      constant-formal-power-series-Commutative-Semiring R
        ( mul-Commutative-Semiring R x y) ＝
      mul-formal-power-series-Commutative-Semiring
        ( constant-formal-power-series-Commutative-Semiring R x)
        ( constant-formal-power-series-Commutative-Semiring R y)
    preserves-mul-constant-formal-power-series-Commutative-Semiring {x} {y} =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( inv
          ( eq-htpy
            ( λ where
              zero-ℕ →
                sum-finite-is-contr-Commutative-Semiring R
                  ( _)
                  ( is-contr-binary-sum-decomposition-zero-ℕ)
                  ( 0 , 0 , refl)
                  ( _)
              (succ-ℕ n) →
                htpy-sum-finite-Commutative-Semiring R
                  ( _)
                  ( λ where
                    (succ-ℕ m , _ , refl) →
                      left-zero-law-mul-Commutative-Semiring R _
                    (zero-ℕ , succ-ℕ n , refl) →
                      right-zero-law-mul-Commutative-Semiring R _) ∙
                sum-zero-finite-Commutative-Semiring R _)))

    preserves-add-constant-formal-power-series-Commutative-Semiring :
      {x y : type-Commutative-Semiring R} →
      constant-formal-power-series-Commutative-Semiring R
        ( add-Commutative-Semiring R x y) ＝
      add-formal-power-series-Commutative-Semiring
        ( constant-formal-power-series-Commutative-Semiring R x)
        ( constant-formal-power-series-Commutative-Semiring R y)
    preserves-add-constant-formal-power-series-Commutative-Semiring =
      ap
        ( formal-power-series-coefficients-Commutative-Semiring)
        ( eq-htpy
          ( λ where
              zero-ℕ → refl
              (succ-ℕ n) → inv (left-unit-law-add-Commutative-Semiring R _)))

  hom-additive-commutative-monoid-constant-formal-power-series-Commutative-Semiring :
    hom-Commutative-Monoid
      ( additive-commutative-monoid-Commutative-Semiring R)
      ( additive-commutative-monoid-formal-power-series-Commutative-Semiring R)
  hom-additive-commutative-monoid-constant-formal-power-series-Commutative-Semiring =
    ( ( constant-formal-power-series-Commutative-Semiring R ,
        preserves-add-constant-formal-power-series-Commutative-Semiring) ,
      constant-zero-formal-power-series-Commutative-Semiring R)

  hom-constant-formal-power-series-Commutative-Semiring :
    hom-Commutative-Semiring
      ( R)
      ( commutative-semiring-formal-power-series-Commutative-Semiring R)
  hom-constant-formal-power-series-Commutative-Semiring =
    ( hom-additive-commutative-monoid-constant-formal-power-series-Commutative-Semiring ,
      preserves-mul-constant-formal-power-series-Commutative-Semiring ,
      constant-one-formal-power-series-Commutative-Semiring R)

Recent changes