# Vectors on commutative rings

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

Created on 2023-02-20.

module linear-algebra.vectors-on-commutative-rings where

Imports
open import commutative-algebra.commutative-rings

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-rings


## Idea

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

## Definitions

### Listed vectors on commutative rings

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

vec-Commutative-Ring : ℕ → UU l
vec-Commutative-Ring = vec-Ring (ring-Commutative-Ring R)

{n : ℕ} → vec-Commutative-Ring (succ-ℕ n) → type-Commutative-Ring R

tail-vec-Commutative-Ring :
{n : ℕ} → vec-Commutative-Ring (succ-ℕ n) → vec-Commutative-Ring n
tail-vec-Commutative-Ring = tail-vec-Ring (ring-Commutative-Ring R)

snoc-vec-Commutative-Ring :
{n : ℕ} → vec-Commutative-Ring n → type-Commutative-Ring R →
vec-Commutative-Ring (succ-ℕ n)
snoc-vec-Commutative-Ring = snoc-vec-Ring (ring-Commutative-Ring R)


### Functional vectors on commutative rings

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

functional-vec-Commutative-Ring : ℕ → UU l
functional-vec-Commutative-Ring =
functional-vec-Ring (ring-Commutative-Ring R)

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

tail-functional-vec-Commutative-Ring :
(n : ℕ) → functional-vec-Commutative-Ring (succ-ℕ n) →
functional-vec-Commutative-Ring n
tail-functional-vec-Commutative-Ring =
tail-functional-vec-Ring (ring-Commutative-Ring R)

cons-functional-vec-Commutative-Ring :
(n : ℕ) → type-Commutative-Ring R →
functional-vec-Commutative-Ring n →
functional-vec-Commutative-Ring (succ-ℕ n)
cons-functional-vec-Commutative-Ring =
cons-functional-vec-Ring (ring-Commutative-Ring R)

snoc-functional-vec-Commutative-Ring :
(n : ℕ) → functional-vec-Commutative-Ring n →
type-Commutative-Ring R → functional-vec-Commutative-Ring (succ-ℕ n)
snoc-functional-vec-Commutative-Ring =
snoc-functional-vec-Ring (ring-Commutative-Ring R)


### Zero vector on a commutative ring

#### The zero listed vector

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

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


#### The zero functional vector

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

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


### Pointwise addition of vectors on a commutative ring

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

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

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

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

vec-Commutative-Ring-Semigroup : ℕ → Semigroup l
vec-Commutative-Ring-Semigroup =
vec-Ring-Semigroup (ring-Commutative-Ring R)

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

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

vec-Commutative-Ring-Monoid : ℕ → Monoid l
vec-Commutative-Ring-Monoid =
vec-Ring-Monoid (ring-Commutative-Ring R)

{n : ℕ} (v w : vec-Commutative-Ring R n) →

vec-Commutative-Ring-Commutative-Monoid : ℕ → Commutative-Monoid l
vec-Commutative-Ring-Commutative-Monoid =
vec-Ring-Commutative-Monoid (ring-Commutative-Ring R)


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

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

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

(n : ℕ) (v1 v2 v3 : functional-vec-Commutative-Ring R n) →
( add-functional-vec-Commutative-Ring n v1 v2) v3) ＝

functional-vec-Commutative-Ring-Semigroup : ℕ → Semigroup l
functional-vec-Commutative-Ring-Semigroup =
functional-vec-Ring-Semigroup (ring-Commutative-Ring R)

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

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

functional-vec-Commutative-Ring-Monoid : ℕ → Monoid l
functional-vec-Commutative-Ring-Monoid =
functional-vec-Ring-Monoid (ring-Commutative-Ring R)