# Vectors on euclidean domains

Content created by Fredrik Bakke, Egbert Rijke and Fernando Chu.

Created on 2023-04-05.

module linear-algebra.vectors-on-euclidean-domains where

Imports
open import commutative-algebra.euclidean-domains

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.unital-binary-operations
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.commutative-monoids
open import group-theory.groups
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


## Idea

Given an euclidean domain R, the type vec n R of R-vectors is an R-module.

## Definitions

### Listed vectors on euclidean domains

module _
{l : Level} (R : Euclidean-Domain l)
where

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

{n : ℕ} → vec-Euclidean-Domain (succ-ℕ n) → type-Euclidean-Domain R

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

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


### Functional vectors on euclidean domains

module _
{l : Level} (R : Euclidean-Domain l)
where

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

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

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

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

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


### Zero vector on a euclidean domain

#### The zero listed vector

module _
{l : Level} (R : Euclidean-Domain l)
where

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


#### The zero functional vector

module _
{l : Level} (R : Euclidean-Domain l)
where

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


### Pointwise addition of vectors on a euclidean domain

#### Pointwise addition of listed vectors on a euclidean domain

module _
{l : Level} (R : Euclidean-Domain l)
where

{n : ℕ} →
vec-Euclidean-Domain R n →
vec-Euclidean-Domain R n →
vec-Euclidean-Domain R n

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

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

{n : ℕ} (v : vec-Euclidean-Domain R n) →
Id (add-vec-Euclidean-Domain (zero-vec-Euclidean-Domain R) v) v
ap-binary _∷_

{n : ℕ} (v : vec-Euclidean-Domain R n) →
Id (add-vec-Euclidean-Domain v (zero-vec-Euclidean-Domain R)) v
ap-binary _∷_

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

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

vec-Euclidean-Domain-Commutative-Monoid : ℕ → Commutative-Monoid l
pr1 (vec-Euclidean-Domain-Commutative-Monoid n) =
vec-Euclidean-Domain-Monoid n
pr2 (vec-Euclidean-Domain-Commutative-Monoid n) =


#### Pointwise addition of functional vectors on a euclidean domain

module _
{l : Level} (R : Euclidean-Domain l)
where

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

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

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

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

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

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

(n : ℕ) (v w : functional-vec-Euclidean-Domain R n) →
eq-htpy (λ i → commutative-add-Euclidean-Domain R (v i) (w i))

functional-vec-Euclidean-Domain-Commutative-Monoid : ℕ → Commutative-Monoid l
pr1 (functional-vec-Euclidean-Domain-Commutative-Monoid n) =
functional-vec-Euclidean-Domain-Monoid n
pr2 (functional-vec-Euclidean-Domain-Commutative-Monoid n) =


### The negative of a vector on a euclidean domain

module _
{l : Level} (R : Euclidean-Domain l)
where

neg-vec-Euclidean-Domain :
{n : ℕ} → vec-Euclidean-Domain R n → vec-Euclidean-Domain R n
neg-vec-Euclidean-Domain = map-vec (neg-Euclidean-Domain R)

{n : ℕ} (v : vec-Euclidean-Domain R n) →
Id
( add-vec-Euclidean-Domain R (neg-vec-Euclidean-Domain v) v)
( zero-vec-Euclidean-Domain R)
ap-binary _∷_

{n : ℕ} (v : vec-Euclidean-Domain R n) →
Id
( add-vec-Euclidean-Domain R v (neg-vec-Euclidean-Domain v))
( zero-vec-Euclidean-Domain R)
ap-binary _∷_

is-unital-vec-Euclidean-Domain :
(n : ℕ) → is-unital (add-vec-Euclidean-Domain R {n})
pr1 (is-unital-vec-Euclidean-Domain n) = zero-vec-Euclidean-Domain R
pr1 (pr2 (is-unital-vec-Euclidean-Domain n)) =
pr2 (pr2 (is-unital-vec-Euclidean-Domain n)) =

is-group-vec-Euclidean-Domain :
(n : ℕ) → is-group-Semigroup (vec-Euclidean-Domain-Semigroup R n)
pr1 (is-group-vec-Euclidean-Domain n) = is-unital-vec-Euclidean-Domain n
pr1 (pr2 (is-group-vec-Euclidean-Domain n)) = neg-vec-Euclidean-Domain
pr1 (pr2 (pr2 (is-group-vec-Euclidean-Domain n))) =