# Vectors on semirings

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

Created on 2023-02-20.

module linear-algebra.vectors-on-semirings where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
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.functoriality-vectors
open import linear-algebra.vectors

open import ring-theory.semirings


## Idea

Given a ring R, the type vec n R of R-vectors is an R-module

## Definitions

### Listed vectors on semirings

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

vec-Semiring : ℕ → UU l
vec-Semiring = vec (type-Semiring R)

head-vec-Semiring : {n : ℕ} → vec-Semiring (succ-ℕ n) → type-Semiring R

tail-vec-Semiring : {n : ℕ} → vec-Semiring (succ-ℕ n) → vec-Semiring n
tail-vec-Semiring v = tail-vec v

snoc-vec-Semiring :
{n : ℕ} → vec-Semiring n → type-Semiring R → vec-Semiring (succ-ℕ n)
snoc-vec-Semiring v r = snoc-vec v r


### Functional vectors on rings

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

functional-vec-Semiring : ℕ → UU l
functional-vec-Semiring = functional-vec (type-Semiring R)

(n : ℕ) → functional-vec-Semiring (succ-ℕ n) → type-Semiring R

tail-functional-vec-Semiring :
(n : ℕ) → functional-vec-Semiring (succ-ℕ n) → functional-vec-Semiring n
tail-functional-vec-Semiring = tail-functional-vec

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

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


### Zero vector on a ring

#### The zero listed vector

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

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


#### The zero functional vector

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

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


### Pointwise addition of vectors on a ring

#### Pointwise addition of listed vectors on a ring

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

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

{n : ℕ} (v1 v2 v3 : vec-Semiring R n) →
associative-add-vec-Semiring empty-vec empty-vec empty-vec = refl
associative-add-vec-Semiring (x ∷ v1) (y ∷ v2) (z ∷ v3) =
ap-binary _∷_
( associative-add-Semiring R x y z)

vec-Semiring-Semigroup : ℕ → Semigroup l
pr1 (vec-Semiring-Semigroup n) = vec-Set (set-Semiring R) n
pr1 (pr2 (vec-Semiring-Semigroup n)) = add-vec-Semiring
pr2 (pr2 (vec-Semiring-Semigroup n)) = associative-add-vec-Semiring

{n : ℕ} (v : vec-Semiring R n) →
add-vec-Semiring (zero-vec-Semiring R) v ＝ v
ap-binary _∷_

{n : ℕ} (v : vec-Semiring R n) →
add-vec-Semiring v (zero-vec-Semiring R) ＝ v
ap-binary _∷_

vec-Semiring-Monoid : ℕ → Monoid l
pr1 (vec-Semiring-Monoid n) = vec-Semiring-Semigroup n
pr1 (pr2 (vec-Semiring-Monoid n)) = zero-vec-Semiring R
pr1 (pr2 (pr2 (vec-Semiring-Monoid n))) = left-unit-law-add-vec-Semiring
pr2 (pr2 (pr2 (vec-Semiring-Monoid n))) = right-unit-law-add-vec-Semiring

{n : ℕ} (v w : vec-Semiring R n) →
commutative-add-vec-Semiring (x ∷ v) (y ∷ w) =
ap-binary _∷_

vec-Semiring-Commutative-Monoid : ℕ → Commutative-Monoid l
pr1 (vec-Semiring-Commutative-Monoid n) = vec-Semiring-Monoid n


#### Pointwise addition of functional vectors on a ring

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

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

(n : ℕ) (v1 v2 v3 : functional-vec-Semiring R n) →
associative-add-functional-vec-Semiring n v1 v2 v3 =
eq-htpy (λ i → associative-add-Semiring R (v1 i) (v2 i) (v3 i))

functional-vec-Semiring-Semigroup : ℕ → Semigroup l
pr1 (functional-vec-Semiring-Semigroup n) =
functional-vec-Set (set-Semiring R) n
pr1 (pr2 (functional-vec-Semiring-Semigroup n)) =
pr2 (pr2 (functional-vec-Semiring-Semigroup n)) =

(n : ℕ) (v : functional-vec-Semiring R n) →
add-functional-vec-Semiring n (zero-functional-vec-Semiring R n) v ＝ v
eq-htpy (λ i → left-unit-law-add-Semiring R (v i))

(n : ℕ) (v : functional-vec-Semiring R n) →
add-functional-vec-Semiring n v (zero-functional-vec-Semiring R n) ＝ v
eq-htpy (λ i → right-unit-law-add-Semiring R (v i))

functional-vec-Semiring-Monoid : ℕ → Monoid l
pr1 (functional-vec-Semiring-Monoid n) =
functional-vec-Semiring-Semigroup n
pr1 (pr2 (functional-vec-Semiring-Monoid n)) =
zero-functional-vec-Semiring R n
pr1 (pr2 (pr2 (functional-vec-Semiring-Monoid n))) =
pr2 (pr2 (pr2 (functional-vec-Semiring-Monoid n))) =