# Vectors on commutative semirings

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2023-02-20.

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 structure 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)

{n : ℕ} → vec-Commutative-Semiring (succ-ℕ n) → type-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)

(n : ℕ) → functional-vec-Commutative-Semiring (succ-ℕ n) →
type-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

{n : ℕ} → vec-Commutative-Semiring R n → vec-Commutative-Semiring R n →
vec-Commutative-Semiring R n

{n : ℕ} (v1 v2 v3 : vec-Commutative-Semiring R n) →

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

{n : ℕ} (v : vec-Commutative-Semiring R n) →
add-vec-Commutative-Semiring (zero-vec-Commutative-Semiring R) v ＝ v

{n : ℕ} (v : vec-Commutative-Semiring R n) →
add-vec-Commutative-Semiring v (zero-vec-Commutative-Semiring R) ＝ v

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

{n : ℕ} (v w : vec-Commutative-Semiring R n) →
add-vec-Commutative-Semiring v w ＝ add-vec-Commutative-Semiring w v

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

(n : ℕ) (v w : functional-vec-Commutative-Semiring R n) →
functional-vec-Commutative-Semiring R n

(n : ℕ) (v1 v2 v3 : functional-vec-Commutative-Semiring R 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))

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

(n : ℕ) (v : functional-vec-Commutative-Semiring R n) →
( zero-functional-vec-Commutative-Semiring R n) v ＝ v

(n : ℕ) (v : functional-vec-Commutative-Semiring R n) →
( zero-functional-vec-Commutative-Semiring R n) ＝ v

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