Vectors on commutative semirings

module linear-algebra.vectors-on-commutative-semirings where
Imports
open import commutative-algebra.commutative-semirings

open import elementary-number-theory.natural-numbers

open import foundation.identity-types
open import foundation.universe-levels

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

open import linear-algebra.constant-vectors
open import linear-algebra.vectors-on-semirings

Idea

Vectors on a commutative semiring R are vectors on the underlying type of R. The commutative semiring structur on R induces further structure on the type of vectors on R.

Definitions

Listed vectors on commutative semirings

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

  vec-Commutative-Semiring :   UU l
  vec-Commutative-Semiring =
    vec-Semiring (semiring-Commutative-Semiring R)

  head-vec-Commutative-Semiring :
    {n : }  vec-Commutative-Semiring (succ-ℕ n)  type-Commutative-Semiring R
  head-vec-Commutative-Semiring =
    head-vec-Semiring (semiring-Commutative-Semiring R)

  tail-vec-Commutative-Semiring :
    {n : }  vec-Commutative-Semiring (succ-ℕ n)  vec-Commutative-Semiring n
  tail-vec-Commutative-Semiring =
    tail-vec-Semiring (semiring-Commutative-Semiring R)

  snoc-vec-Commutative-Semiring :
    {n : }  vec-Commutative-Semiring n  type-Commutative-Semiring R 
    vec-Commutative-Semiring (succ-ℕ n)
  snoc-vec-Commutative-Semiring =
    snoc-vec-Semiring (semiring-Commutative-Semiring R)

Functional vectors on commutative semirings

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

  functional-vec-Commutative-Semiring :   UU l
  functional-vec-Commutative-Semiring =
    functional-vec-Semiring (semiring-Commutative-Semiring R)

  head-functional-vec-Commutative-Semiring :
    (n : )  functional-vec-Commutative-Semiring (succ-ℕ n) 
    type-Commutative-Semiring R
  head-functional-vec-Commutative-Semiring =
    head-functional-vec-Semiring (semiring-Commutative-Semiring R)

  tail-functional-vec-Commutative-Semiring :
    (n : )  functional-vec-Commutative-Semiring (succ-ℕ n) 
    functional-vec-Commutative-Semiring n
  tail-functional-vec-Commutative-Semiring =
    tail-functional-vec-Semiring (semiring-Commutative-Semiring R)

  cons-functional-vec-Commutative-Semiring :
    (n : )  type-Commutative-Semiring R 
    functional-vec-Commutative-Semiring n 
    functional-vec-Commutative-Semiring (succ-ℕ n)
  cons-functional-vec-Commutative-Semiring =
    cons-functional-vec-Semiring (semiring-Commutative-Semiring R)

  snoc-functional-vec-Commutative-Semiring :
    (n : )  functional-vec-Commutative-Semiring n 
    type-Commutative-Semiring R  functional-vec-Commutative-Semiring (succ-ℕ n)
  snoc-functional-vec-Commutative-Semiring =
    snoc-functional-vec-Semiring (semiring-Commutative-Semiring R)

Zero vector on a commutative semiring

The zero listed vector

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

  zero-vec-Commutative-Semiring : {n : }  vec-Commutative-Semiring R n
  zero-vec-Commutative-Semiring = constant-vec (zero-Commutative-Semiring R)

The zero functional vector

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

  zero-functional-vec-Commutative-Semiring :
    (n : )  functional-vec-Commutative-Semiring R n
  zero-functional-vec-Commutative-Semiring n i = zero-Commutative-Semiring R

Pointwise addition of vectors on a commutative semiring

Pointwise addition of listed vectors on a commutative semiring

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

  add-vec-Commutative-Semiring :
    {n : }  vec-Commutative-Semiring R n  vec-Commutative-Semiring R n 
    vec-Commutative-Semiring R n
  add-vec-Commutative-Semiring =
    add-vec-Semiring (semiring-Commutative-Semiring R)

  associative-add-vec-Commutative-Semiring :
    {n : } (v1 v2 v3 : vec-Commutative-Semiring R n) 
    add-vec-Commutative-Semiring (add-vec-Commutative-Semiring v1 v2) v3 
    add-vec-Commutative-Semiring v1 (add-vec-Commutative-Semiring v2 v3)
  associative-add-vec-Commutative-Semiring =
    associative-add-vec-Semiring (semiring-Commutative-Semiring R)

  vec-Commutative-Semiring-Semigroup :   Semigroup l
  vec-Commutative-Semiring-Semigroup =
    vec-Semiring-Semigroup (semiring-Commutative-Semiring R)

  left-unit-law-add-vec-Commutative-Semiring :
    {n : } (v : vec-Commutative-Semiring R n) 
    add-vec-Commutative-Semiring (zero-vec-Commutative-Semiring R) v  v
  left-unit-law-add-vec-Commutative-Semiring =
    left-unit-law-add-vec-Semiring (semiring-Commutative-Semiring R)

  right-unit-law-add-vec-Commutative-Semiring :
    {n : } (v : vec-Commutative-Semiring R n) 
    add-vec-Commutative-Semiring v (zero-vec-Commutative-Semiring R)  v
  right-unit-law-add-vec-Commutative-Semiring =
    right-unit-law-add-vec-Semiring (semiring-Commutative-Semiring R)

  vec-Commutative-Semiring-Monoid :   Monoid l
  vec-Commutative-Semiring-Monoid =
    vec-Semiring-Monoid (semiring-Commutative-Semiring R)

  commutative-add-vec-Commutative-Semiring :
    {n : } (v w : vec-Commutative-Semiring R n) 
    add-vec-Commutative-Semiring v w  add-vec-Commutative-Semiring w v
  commutative-add-vec-Commutative-Semiring =
    commutative-add-vec-Semiring (semiring-Commutative-Semiring R)

  vec-Commutative-Semiring-Commutative-Monoid :   Commutative-Monoid l
  vec-Commutative-Semiring-Commutative-Monoid =
    vec-Semiring-Commutative-Monoid (semiring-Commutative-Semiring R)

Pointwise addition of functional vectors on a commutative semiring

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

  add-functional-vec-Commutative-Semiring :
    (n : ) (v w : functional-vec-Commutative-Semiring R n) 
    functional-vec-Commutative-Semiring R n
  add-functional-vec-Commutative-Semiring =
    add-functional-vec-Semiring (semiring-Commutative-Semiring R)

  associative-add-functional-vec-Commutative-Semiring :
    (n : ) (v1 v2 v3 : functional-vec-Commutative-Semiring R n) 
    ( add-functional-vec-Commutative-Semiring n
      ( add-functional-vec-Commutative-Semiring n v1 v2) v3) 
    ( add-functional-vec-Commutative-Semiring n v1
      ( add-functional-vec-Commutative-Semiring n v2 v3))
  associative-add-functional-vec-Commutative-Semiring =
    associative-add-functional-vec-Semiring (semiring-Commutative-Semiring R)

  functional-vec-Commutative-Semiring-Semigroup :   Semigroup l
  functional-vec-Commutative-Semiring-Semigroup =
    functional-vec-Semiring-Semigroup (semiring-Commutative-Semiring R)

  left-unit-law-add-functional-vec-Commutative-Semiring :
    (n : ) (v : functional-vec-Commutative-Semiring R n) 
    add-functional-vec-Commutative-Semiring n
      ( zero-functional-vec-Commutative-Semiring R n) v  v
  left-unit-law-add-functional-vec-Commutative-Semiring =
    left-unit-law-add-functional-vec-Semiring (semiring-Commutative-Semiring R)

  right-unit-law-add-functional-vec-Commutative-Semiring :
    (n : ) (v : functional-vec-Commutative-Semiring R n) 
    add-functional-vec-Commutative-Semiring n v
      ( zero-functional-vec-Commutative-Semiring R n)  v
  right-unit-law-add-functional-vec-Commutative-Semiring =
    right-unit-law-add-functional-vec-Semiring (semiring-Commutative-Semiring R)

  functional-vec-Commutative-Semiring-Monoid :   Monoid l
  functional-vec-Commutative-Semiring-Monoid =
    functional-vec-Semiring-Monoid (semiring-Commutative-Semiring R)

  commutative-add-functional-vec-Commutative-Semiring :
    (n : ) (v w : functional-vec-Commutative-Semiring R n) 
    add-functional-vec-Commutative-Semiring n v w 
    add-functional-vec-Commutative-Semiring n w v
  commutative-add-functional-vec-Commutative-Semiring =
    commutative-add-functional-vec-Semiring (semiring-Commutative-Semiring R)

  functional-vec-Commutative-Semiring-Commutative-Monoid :
      Commutative-Monoid l
  functional-vec-Commutative-Semiring-Commutative-Monoid =
    functional-vec-Semiring-Commutative-Monoid (semiring-Commutative-Semiring R)