Sequences in semirings

Content created by Elif Uskuplu and malarbol.

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

module ring-theory.sequences-semirings where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-products-propositions
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.commuting-elements-monoids
open import group-theory.semigroups

open import lists.sequences

open import ring-theory.function-semirings
open import ring-theory.semirings

Idea

The type of sequences in a semiring inherits the function semiring structure with pointwise addition and multiplication. This is the semiring of sequences in a semiring.

Definition

The semiring of sequences in a semiring with pointwise operations

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

  sequence-Semiring : Semiring l
  sequence-Semiring = function-Semiring R ℕ

  type-sequence-Semiring : UU l
  type-sequence-Semiring = type-Semiring sequence-Semiring

  additive-commutative-monoid-sequence-Semiring : Commutative-Monoid l
  additive-commutative-monoid-sequence-Semiring =
    additive-commutative-monoid-Semiring sequence-Semiring

  zero-sequence-Semiring : type-sequence-Semiring
  zero-sequence-Semiring = zero-Semiring sequence-Semiring

  add-sequence-Semiring :
    type-sequence-Semiring → type-sequence-Semiring → type-sequence-Semiring
  add-sequence-Semiring =
    add-Semiring sequence-Semiring

Recent changes