# Multiplication of matrices

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

Created on 2022-03-16.

module linear-algebra.multiplication-matrices where

Imports

## Definition

### Multiplication of matrices

{-
mul-vector-matrix : {l : Level} → {K : UU l} → {m n : ℕ} →
(K → K → K) → (K → K → K) → K →
vec K m → Mat K m n → vec K n
mul-vector-matrix _ _ zero empty-vec empty-vec = diagonal-product zero
mul-vector-matrix mulK addK zero (x ∷ xs) (v ∷ vs) =
(mul-vector-matrix mulK addK zero xs vs)

mul-Mat : {l' : Level} → {K : UU l'} → {l m n : ℕ} →
(K → K → K) → (K → K → K) → K →
Mat K l m → Mat K m n → Mat K l n
mul-Mat _ _ zero empty-vec _ = empty-vec
mul-Mat mulK addK zero (v ∷ vs) m =
mul-vector-matrix mulK addK zero v m
∷ mul-Mat mulK addK zero vs m
-}


## Properties

{-
mul-transpose :
{l : Level} → {K : UU l} → {m n p : ℕ} →
{addK : K → K → K} {mulK : K → K → K} {zero : K} →
((x y : K) → Id (mulK x y) (mulK y x)) →
(a : Mat K m n) → (b : Mat K n p) →
Id
(transpose (mul-Mat mulK addK zero a b))
(mul-Mat mulK addK zero (transpose b) (transpose a))
mul-transpose mulK-comm empty-vec b = {!!}
mul-transpose mulK-comm (a ∷ as) b = {!!}
-}


## Properties of Matrix Multiplication

• distributive laws (incomplete)
• associativity (TODO)
• identity (TODO)
{-
module _
{l : Level}
{K : UU l}
{addK : K → K → K}
{mulK : K → K → K}
{zero : K}
where

left-distributive-vector-matrix :
{n m : ℕ} →
({l : ℕ} →  Id (diagonal-product {n = l} zero)
((x y z : K) → (Id (mulK x (addK y z)) (addK (mulK x y) (mulK x z)))) →
((x y : K) → Id (addK x y) (addK y x)) →
(a : vec K n) (b : Mat K n m) (c : Mat K n m) →
(mul-vector-matrix mulK addK zero a c))
left-distributive-vector-matrix id-vec _ _ _ empty-vec empty-vec empty-vec =
id-vec
left-distributive-vector-matrix
id-vec k-distr addK-comm addK-associative (a ∷ as) (r1 ∷ r1s) (r2 ∷ r2s) =
ap
( λ r →
(left-distributive-scalar-vector {zero = zero} k-distr a r1 r2)
(mul-scalar-vector mulK a r2)) r)
(left-distributive-vector-matrix
∙ lemma-shuffle)
where
lemma-shuffle : {n : ℕ} →
{x y z w : vec K n} →
lemma-shuffle {x = x} {y = y} {z = z} {w = w} =

left-distributive-matrices :
{n m p : ℕ} →
({l : ℕ} →
Id
(diagonal-product {n = l} zero)
((x y z : K) → (Id (mulK x (addK y z)) (addK (mulK x y) (mulK x z)))) →
((x y : K) → Id (addK x y) (addK y x)) →
(a : Mat K m n) (b : Mat K n p) (c : Mat K n p) →
(mul-Mat mulK addK zero a c))
left-distributive-matrices _ _ _ _ empty-vec _ _ = refl
(left-distributive-vector-matrix
(mul-vector-matrix mulK addK zero a c)))
(left-distributive-matrices
-}

{- TODO: right distributivity
right-distributive-matrices :
{n m p : ℕ} →
({l : ℕ} →
Id
(diagonal-product {n = l} zero)
((x y z : K) → (Id (mulK (addK x y) z) (addK (mulK x z) (mulK y z)))) →
((x y : K) → Id (addK x y) (addK y x)) →
(b : Mat K n p) (c : Mat K n p) (d : Mat K p m) →
(mul-Mat mulK addK zero c d))
right-distributive-matrices _ _ _ _ empty-vec empty-vec _ = refl
right-distributive-matrices
{p = .zero-ℕ}
id-vec k-distr addK-comm addK-associative (b ∷ bs) (c ∷ cs) empty-vec =
{!!}
right-distributive-matrices
id-vec k-distr addK-comm addK-associative (b ∷ bs) (c ∷ cs) (d ∷ ds) =
{!!}
-- this might also need a proof that zero is the additive identity

TODO: associativity
associative-mul-matrices :
{l : Level} {K : UU l} {n m p q : ℕ} →
{addK : K → K → K} {mulK : K → K → K} {zero : K} →
(x : Mat K m n) → (y : Mat K n p) → (z : Mat K p q) →
Id (mul-Mat mulK addK zero x (mul-Mat mulK addK zero y z))