Vectors on rings

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Dylan Braithwaite, Erik Schnetter, Fernando Chu and Victor Blanchi.

Created on 2022-03-15.

module linear-algebra.vectors-on-rings 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.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

open import ring-theory.rings


Idea

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

Definitions

Listed vectors on rings

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

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

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

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

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


Functional vectors on rings

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

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

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

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

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

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


Zero vector on a ring

The zero listed vector

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

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


The zero functional vector

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

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


Pointwise addition of vectors on a ring

Pointwise addition of listed vectors on a ring

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

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

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

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

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

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

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

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

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


Pointwise addition of functional vectors on a ring

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

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

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

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

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

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

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

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

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


The negative of a vector on a ring

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

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

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

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

is-unital-vec-Ring : (n : ℕ) → is-unital (add-vec-Ring R {n})
pr1 (is-unital-vec-Ring n) = zero-vec-Ring R
pr1 (pr2 (is-unital-vec-Ring n)) = left-unit-law-add-vec-Ring R
pr2 (pr2 (is-unital-vec-Ring n)) = right-unit-law-add-vec-Ring R

is-group-vec-Ring : (n : ℕ) → is-group-Semigroup (vec-Ring-Semigroup R n)
pr1 (is-group-vec-Ring n) = is-unital-vec-Ring n
pr1 (pr2 (is-group-vec-Ring n)) = neg-vec-Ring
pr1 (pr2 (pr2 (is-group-vec-Ring n))) = left-inverse-law-add-vec-Ring
pr2 (pr2 (pr2 (is-group-vec-Ring n))) = right-inverse-law-add-vec-Ring

vec-Ring-Group : ℕ → Group l
pr1 (vec-Ring-Group n) = vec-Ring-Semigroup R n
pr2 (vec-Ring-Group n) = is-group-vec-Ring n

vec-Ring-Ab : ℕ → Ab l
pr1 (vec-Ring-Ab n) = vec-Ring-Group n
pr2 (vec-Ring-Ab n) = commutative-add-vec-Ring R