Vectors on semirings

module linear-algebra.vectors-on-semirings where
Imports
open import elementary-number-theory.natural-numbers

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
  head-vec-Semiring v = head-vec v

  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)

  head-functional-vec-Semiring :
    (n : )  functional-vec-Semiring (succ-ℕ n)  type-Semiring R
  head-functional-vec-Semiring n v = head-functional-vec n v

  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

  add-vec-Semiring :
    {n : }  vec-Semiring R n  vec-Semiring R n  vec-Semiring R n
  add-vec-Semiring = binary-map-vec (add-Semiring R)

  associative-add-vec-Semiring :
    {n : } (v1 v2 v3 : vec-Semiring R n) 
    add-vec-Semiring (add-vec-Semiring v1 v2) v3 
    add-vec-Semiring v1 (add-vec-Semiring v2 v3)
  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)
      ( associative-add-vec-Semiring v1 v2 v3)

  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

  left-unit-law-add-vec-Semiring :
    {n : } (v : vec-Semiring R n) 
    add-vec-Semiring (zero-vec-Semiring R) v  v
  left-unit-law-add-vec-Semiring empty-vec = refl
  left-unit-law-add-vec-Semiring (x  v) =
    ap-binary _∷_
      ( left-unit-law-add-Semiring R x)
      ( left-unit-law-add-vec-Semiring v)

  right-unit-law-add-vec-Semiring :
    {n : } (v : vec-Semiring R n) 
    add-vec-Semiring v (zero-vec-Semiring R)  v
  right-unit-law-add-vec-Semiring empty-vec = refl
  right-unit-law-add-vec-Semiring (x  v) =
    ap-binary _∷_
      ( right-unit-law-add-Semiring R x)
      ( right-unit-law-add-vec-Semiring v)

  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

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

  vec-Semiring-Commutative-Monoid :   Commutative-Monoid l
  pr1 (vec-Semiring-Commutative-Monoid n) = vec-Semiring-Monoid n
  pr2 (vec-Semiring-Commutative-Monoid n) = commutative-add-vec-Semiring

Pointwise addition of functional vectors on a ring

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

  add-functional-vec-Semiring :
    (n : ) (v w : functional-vec-Semiring R n)  functional-vec-Semiring R n
  add-functional-vec-Semiring n = binary-map-functional-vec n (add-Semiring R)

  associative-add-functional-vec-Semiring :
    (n : ) (v1 v2 v3 : functional-vec-Semiring R n) 
    ( add-functional-vec-Semiring n (add-functional-vec-Semiring n v1 v2) v3) 
    ( add-functional-vec-Semiring n v1 (add-functional-vec-Semiring n v2 v3))
  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)) =
    add-functional-vec-Semiring n
  pr2 (pr2 (functional-vec-Semiring-Semigroup n)) =
    associative-add-functional-vec-Semiring n

  left-unit-law-add-functional-vec-Semiring :
    (n : ) (v : functional-vec-Semiring R n) 
    add-functional-vec-Semiring n (zero-functional-vec-Semiring R n) v  v
  left-unit-law-add-functional-vec-Semiring n v =
    eq-htpy  i  left-unit-law-add-Semiring R (v i))

  right-unit-law-add-functional-vec-Semiring :
    (n : ) (v : functional-vec-Semiring R n) 
    add-functional-vec-Semiring n v (zero-functional-vec-Semiring R n)  v
  right-unit-law-add-functional-vec-Semiring 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))) =
    left-unit-law-add-functional-vec-Semiring n
  pr2 (pr2 (pr2 (functional-vec-Semiring-Monoid n))) =
    right-unit-law-add-functional-vec-Semiring n

  commutative-add-functional-vec-Semiring :
    (n : ) (v w : functional-vec-Semiring R n) 
    add-functional-vec-Semiring n v w  add-functional-vec-Semiring n w v
  commutative-add-functional-vec-Semiring n v w =
    eq-htpy  i  commutative-add-Semiring R (v i) (w i))

  functional-vec-Semiring-Commutative-Monoid :   Commutative-Monoid l
  pr1 (functional-vec-Semiring-Commutative-Monoid n) =
    functional-vec-Semiring-Monoid n
  pr2 (functional-vec-Semiring-Commutative-Monoid n) =
    commutative-add-functional-vec-Semiring n