Multiplication of matrices
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Louis Wasserman.
Created on 2022-03-16.
Last modified on 2025-05-14.
module linear-algebra.multiplication-matrices where
Imports
Definition
Multiplication of matrices
{- mul-tuple-matrix : {l : Level} → {K : UU l} → {m n : ℕ} → (K → K → K) → (K → K → K) → K → tuple K m → Mat K m n → tuple K n mul-tuple-matrix _ _ zero empty-tuple empty-tuple = diagonal-product zero mul-tuple-matrix mulK addK zero (x ∷ xs) (v ∷ vs) = add-tuple addK (mul-scalar-tuple mulK x v) (mul-tuple-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-tuple _ = empty-tuple mul-Mat mulK addK zero (v ∷ vs) m = mul-tuple-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-tuple 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-tuple-matrix : {n m : ℕ} → ({l : ℕ} → Id (diagonal-product {n = l} zero) (add-tuple addK (diagonal-product zero) (diagonal-product 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)) → ((x y z : K) → Id (addK x (addK y z)) (addK (addK x y) z)) → (a : tuple K n) (b : Mat K n m) (c : Mat K n m) → Id (mul-tuple-matrix mulK addK zero a (add-Mat addK b c)) (add-tuple addK (mul-tuple-matrix mulK addK zero a b) (mul-tuple-matrix mulK addK zero a c)) left-distributive-tuple-matrix id-tuple _ _ _ empty-tuple empty-tuple empty-tuple = id-tuple left-distributive-tuple-matrix id-tuple k-distr addK-comm addK-associative (a ∷ as) (r1 ∷ r1s) (r2 ∷ r2s) = ap ( λ r → add-tuple addK r (mul-tuple-matrix mulK addK zero as (add-Mat addK r1s r2s))) (left-distributive-scalar-tuple {zero = zero} k-distr a r1 r2) ∙ (ap (λ r → add-tuple addK (add-tuple addK (map-tuple (mulK a) r1) (mul-scalar-tuple mulK a r2)) r) (left-distributive-tuple-matrix id-tuple k-distr addK-comm addK-associative as r1s r2s) ∙ lemma-shuffle) where lemma-shuffle : {n : ℕ} → {x y z w : tuple K n} → Id (add-tuple addK (add-tuple addK x y) (add-tuple addK z w)) (add-tuple addK (add-tuple addK x z) (add-tuple addK y w)) lemma-shuffle {x = x} {y = y} {z = z} {w = w} = associative-add-tuples {zero = zero} addK-associative (add-tuple addK x y) z w ∙ (commutative-add-tuples {zero = zero} addK-comm (add-tuple addK (add-tuple addK x y) z) w ∙ (associative-add-tuples {zero = zero} addK-associative w (add-tuple addK x y) z ∙ (ap (λ v → add-tuple addK (add-tuple addK w v) z) (commutative-add-tuples {zero = zero} addK-comm x y) ∙ (ap (λ v → add-tuple addK v z) (associative-add-tuples {zero = zero} addK-associative w y x) ∙ (ap (λ v → add-tuple addK (add-tuple addK v x) z) (commutative-add-tuples {zero = zero} addK-comm w y) ∙ (inv (associative-add-tuples {zero = zero} addK-associative (add-tuple addK y w) x z) ∙ commutative-add-tuples {zero = zero} addK-comm (add-tuple addK y w) (add-tuple addK x z))))))) left-distributive-matrices : {n m p : ℕ} → ({l : ℕ} → Id (diagonal-product {n = l} zero) (add-tuple addK (diagonal-product zero) (diagonal-product 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)) → ((x y z : K) → Id (addK x (addK y z)) (addK (addK x y) z)) → (a : Mat K m n) (b : Mat K n p) (c : Mat K n p) → Id (mul-Mat mulK addK zero a (add-Mat addK b c)) (add-Mat addK (mul-Mat mulK addK zero a b) (mul-Mat mulK addK zero a c)) left-distributive-matrices _ _ _ _ empty-tuple _ _ = refl left-distributive-matrices id-tuple k-distr addK-comm addK-associative (a ∷ as) b c = (ap (λ r → r ∷ mul-Mat mulK addK zero as (add-Mat addK b c)) (left-distributive-tuple-matrix id-tuple k-distr addK-comm addK-associative a b c)) ∙ ap (_∷_ (add-tuple addK (mul-tuple-matrix mulK addK zero a b) (mul-tuple-matrix mulK addK zero a c))) (left-distributive-matrices id-tuple k-distr addK-comm addK-associative as b c) -} {- TODO: right distributivity right-distributive-matrices : {n m p : ℕ} → ({l : ℕ} → Id (diagonal-product {n = l} zero) (add-tuple addK (diagonal-product zero) (diagonal-product 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)) → ((x y z : K) → Id (addK x (addK y z)) (addK (addK x y) z)) → (b : Mat K n p) (c : Mat K n p) (d : Mat K p m) → Id (mul-Mat mulK addK zero (add-Mat addK b c) d) (add-Mat addK (mul-Mat mulK addK zero b d) (mul-Mat mulK addK zero c d)) right-distributive-matrices _ _ _ _ empty-tuple empty-tuple _ = refl right-distributive-matrices {p = .zero-ℕ} id-tuple k-distr addK-comm addK-associative (b ∷ bs) (c ∷ cs) empty-tuple = {!!} right-distributive-matrices id-tuple 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)) (mul-Mat mulK addK zero (mul-Mat mulK addK zero x y) z) associative-mul-matrices x y z = {!!} -}
Recent changes
- 2025-05-14. Louis Wasserman. Refactor linear algebra to use “tuples” for what was “vectors” (#1397).
- 2024-04-11. Fredrik Bakke. Refactor diagonals (#1096).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).