Convolution of sequences in rings

Content created by Elif Uskuplu and malarbol.

Created on 2026-09-17.
Last modified on 2026-09-17.

module ring-theory.convolution-sequences-rings where
Imports 
open import foundation.dependent-pair-types
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.semigroups

open import ring-theory.convolution-sequences-semirings
open import ring-theory.rings
open import ring-theory.semirings
open import ring-theory.sequences-rings

Idea

The convolution product of two sequences aₙ and bₙ in a ring is the sequence c = a ⋆ b defined by:

  cₙ = ∑_{0 ≤ i ≤ n} aᵢ bₙ₋ᵢ

With pointwise addition, this forms the convolution ring of sequences in a ring.

Definition

The ring of sequences in a ring under convolution

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

  mul-convolution-sequence-Ring :
    type-sequence-Ring R →
    type-sequence-Ring R →
    type-sequence-Ring R
  mul-convolution-sequence-Ring =
    mul-convolution-sequence-Semiring (semiring-Ring R)

  has-associative-mul-convolution-sequence-Ring :
    has-associative-mul (type-sequence-Ring R)
  has-associative-mul-convolution-sequence-Ring =
    has-associative-mul-convolution-sequence-Semiring (semiring-Ring R)

  is-unital-mul-convolution-sequence-Ring :
    is-unital mul-convolution-sequence-Ring
  is-unital-mul-convolution-sequence-Ring =
    is-unital-mul-convolution-sequence-Semiring (semiring-Ring R)

  convolution-sequence-Ring : Ring l
  convolution-sequence-Ring =
    ( ab-sequence-Ring R ,
      has-associative-mul-convolution-sequence-Ring ,
      is-unital-mul-convolution-sequence-Ring ,
      left-distributive-convolution-add-sequence-Semiring (semiring-Ring R) ,
      right-distributive-convolution-add-sequence-Semiring (semiring-Ring R))

Recent changes