# Matrices

Operations on vectors and matrices.
Author: Langston Barrett (@siddharthist) (March 2018)

## Contents

• Vectors
• Standard conditions on one binary operation
• Standard conditions on a pair of binary operations
• Structures
• Matrices
• Standard conditions on one binary operation
• Structures
• Matrix rig

## Vectors

Definition pointwise {X : UU} (n : nat) (op : binop X) : binop (Vector X n) :=
λ v1 v2 i, op (v1 i) (v2 i).

### Standard conditions on one binary operation

Most features of binary operations (associativity, unity, etc) carry over to pointwise operations.
Section OneOp.
Context {X : UU} {n : nat} {op : binop X}.

Definition pointwise_assoc (assocax : isassoc op) : isassoc (pointwise n op).
Proof.
intros ? ? ?; apply funextfun; intro; apply assocax.
Defined.

Definition pointwise_lunit (lun : X) (lunax : islunit op lun) :
islunit (pointwise n op) (const_vec lun).
Proof.
intros ?; apply funextfun; intro; apply lunax.
Defined.

Definition pointwise_runit (run : X) (runax : isrunit op run) :
isrunit (pointwise n op) (const_vec run).
Proof.
intros ?; apply funextfun; intro; apply runax.
Defined.

Definition pointwise_unit (un : X) (unax : isunit op un) :
isunit (pointwise n op) (const_vec un).
Proof.
use make_isunit.
- apply pointwise_lunit; exact (pr1 unax).
- apply pointwise_runit; exact (pr2 unax).
Defined.

Definition pointwise_comm (commax : iscomm op) : iscomm (pointwise n op).
Proof.
intros ? ?; apply funextfun; intro; apply commax.
Defined.

Definition pointwise_monoidop (monoidax : ismonoidop op) :
ismonoidop (pointwise n op).
Proof.
use make_ismonoidop.
- apply pointwise_assoc, assocax_is; assumption.
- use make_isunital.
+ apply (const_vec (unel_is monoidax)).
+ apply pointwise_unit, unax_is.
Defined.

Definition pointwise_abmonoidop (abmonoidax : isabmonoidop op) :
isabmonoidop (pointwise n op).
Proof.
use make_isabmonoidop.
- apply pointwise_monoidop; exact (pr1isabmonoidop _ _ abmonoidax).
- apply pointwise_comm; exact (pr2 abmonoidax).
Defined.

End OneOp.

### Standard conditions on a pair of binary operations

Section TwoOps.
Context {X : UU} {n : nat} {op : binop X} {op' : binop X}.

Definition pointwise_ldistr (isldistrax : isldistr op op') :
isldistr (pointwise n op) (pointwise n op').
Proof.
intros ? ? ?; apply funextfun; intro; apply isldistrax.
Defined.

Definition pointwise_rdistr (isrdistrax : isrdistr op op') :
isrdistr (pointwise n op) (pointwise n op').
Proof.
intros ? ? ?; apply funextfun; intro; apply isrdistrax.
Defined.

Definition pointwise_distr (isdistrax : isdistr op op') :
isdistr (pointwise n op) (pointwise n op').
Proof.
use make_dirprod.
- apply pointwise_ldistr; apply (dirprod_pr1 isdistrax).
- apply pointwise_rdistr; apply (dirprod_pr2 isdistrax).
Defined.

End TwoOps.

### Structures

Section Structures.

Definition pointwise_hSet (X : hSet) (n : nat) : hSet.
Proof.
use make_hSet.
- exact (Vector X n).
- change isaset with (isofhlevel 2).
apply vector_hlevel, setproperty.
Defined.

Definition pointwise_setwithbinop (X : setwithbinop) (n : nat) : setwithbinop.
Proof.
use make_setwithbinop.
- apply pointwise_hSet; [exact X|assumption].
- exact (pointwise n op).
Defined.

Definition pointwise_setwith2binop (X : setwith2binop) (n : nat) : setwith2binop.
Proof.
use make_setwith2binop.
- apply pointwise_hSet; [exact X|assumption].
- split.
+ exact (pointwise n op1).
+ exact (pointwise n op2).
Defined.

Definition pointwise_monoid (X : monoid) (n : nat) : monoid.
Proof.
use make_monoid.
- apply pointwise_setwithbinop; [exact X|assumption].
- apply pointwise_monoidop; exact (pr2 X).
Defined.

Definition pointwise_abmonoid (X : abmonoid) (n : nat) : abmonoid.
Proof.
use make_abmonoid.
- apply pointwise_setwithbinop; [exact X|assumption].
- apply pointwise_abmonoidop; exact (pr2 X).
Defined.

End Structures.

## Matrices

Definition entrywise {X : UU} (n m : nat) (op : binop X) : binop (Matrix X n m) :=
λ mat1 mat2 i, pointwise _ op (mat1 i) (mat2 i).

### Standard conditions on one binary operation

Section OneOpMat.
Context {X : UU} {n m : nat} {op : binop X}.

Definition entrywise_assoc (assocax : isassoc op) : isassoc (entrywise n m op).
Proof.
intros ? ? ?; apply funextfun; intro; apply pointwise_assoc, assocax.
Defined.

Definition entrywise_lunit (lun : X) (lunax : islunit op lun) :
islunit (entrywise n m op) (const_matrix lun).
Proof.
intros ?; apply funextfun; intro; apply pointwise_lunit, lunax.
Defined.

Definition entrywise_runit (run : X) (runax : isrunit op run) :
isrunit (entrywise n m op) (const_matrix run).
Proof.
intros ?; apply funextfun; intro; apply pointwise_runit, runax.
Defined.

Definition entrywise_unit (un : X) (unax : isunit op un) :
isunit (entrywise n m op) (const_matrix un).
Proof.
use make_isunit.
- apply entrywise_lunit; exact (pr1 unax).
- apply entrywise_runit; exact (pr2 unax).
Defined.

Definition entrywise_comm (commax : iscomm op) : iscomm (entrywise n m op).
Proof.
intros ? ?; apply funextfun; intro; apply pointwise_comm, commax.
Defined.

Definition entrywise_monoidop (monoidax : ismonoidop op) :
ismonoidop (entrywise n m op).
Proof.
use make_ismonoidop.
- apply entrywise_assoc, assocax_is; assumption.
- use make_isunital.
+ apply (const_matrix (unel_is monoidax)).
+ apply entrywise_unit, unax_is.
Defined.

Definition entrywise_abmonoidop (abmonoidax : isabmonoidop op) :
isabmonoidop (entrywise n m op).
Proof.
use make_isabmonoidop.
- apply entrywise_monoidop; exact (pr1isabmonoidop _ _ abmonoidax).
- apply entrywise_comm; exact (pr2 abmonoidax).
Defined.

End OneOpMat.

It is uncommon to consider two entrywise binary operations on matrices, so we don't derive "standard conditions on a pair of binar operations" for matrices.

### Matrix rig

Section MatrixMult.

Context {R : rig}.

Summation and pointwise multiplication
Local Notation Σ := (iterop_fun rigunel1 op1).
Local Notation "R1 ^ R2" := ((pointwise _ op2) R1 R2).

If A is m × n (so B is n × p), AB(i, j) = A(i, 1) * B(1, j) + A(i, 2) * B(2, j) + ⋯ + A(i, n) * B(n, j)
The order of the arguments allows currying the first matrix.
Definition matrix_mult {m n : nat} (mat1 : Matrix R m n)
{p : nat} (mat2 : Matrix R n p) : (Matrix R m p) :=
λ i j, Σ ((row mat1 i) ^ (col mat2 j)).

Local Notation "A ** B" := (matrix_mult A B) (at level 80).

Lemma identity_matrix {n : nat} : (Matrix R n n).
Proof.
intros i j.
induction (stn_eq_or_neq i j).
- exact (rigunel2).     - exact (rigunel1).   Defined.

End MatrixMult.

Local Notation Σ := (iterop_fun rigunel1 op1).
Local Notation "R1 ^ R2" := ((pointwise _ op2) R1 R2).
Local Notation "A ** B" := (matrix_mult A B) (at level 80).

The following is based on "The magnitude of metric spaces" by Tom Leinster (arXiv:1012.5857v3).
Section Weighting.

Context {R : rig}.

Definition 1.1.1 in arXiv:1012.5857v3
Definition weighting {m n : nat} (mat : Matrix R m n) : UU :=
vec : Vector R n, (mat ** (col_vec vec)) = col_vec (const_vec (1%rig)).

Definition coweighting {m n : nat} (mat : Matrix R m n) : UU :=
vec : Vector R m, ((row_vec vec) ** mat) = row_vec (const_vec (1%rig)).

Lemma matrix_mult_vectors {n : nat} (vec1 vec2 : Vector R n) :
((row_vec vec1) ** (col_vec vec2)) = weq_matrix_1_1 (Σ (vec1 ^ vec2)).
Proof.
apply funextfun; intro i; apply funextfun; intro j; reflexivity.
Defined.

Multiplying a column vector by the identity row vector is the same as taking the sum of its entries.
Local Lemma sum_entries1 {n : nat} (vec : Vector R n) :
weq_matrix_1_1 (Σ vec) = ((row_vec (const_vec (1%rig))) ** (col_vec vec)).
Proof.
refine (_ @ !matrix_mult_vectors _ _).
do 2 apply maponpaths.
apply pathsinv0.
refine (pointwise_lunit 1%rig _ vec).
apply riglunax2.
Defined.

Local Lemma sum_entries2 {n : nat} (vec : Vector R n) :
weq_matrix_1_1 (Σ vec) = (row_vec vec ** col_vec (const_vec 1%rig)).
Proof.
refine (_ @ !matrix_mult_vectors _ _).
do 2 apply maponpaths.
apply pathsinv0.
refine (pointwise_runit 1%rig _ vec).
apply rigrunax2.
Defined.

TODO: prove this so that the below isn't hypothetical
Definition matrix_mult_assoc_statement : UU :=
(m n : nat) (mat1 : Matrix R m n)
(p : nat) (mat2 : Matrix R n p)
(q : nat) (mat3 : Matrix R p q),
((mat1 ** mat2) ** mat3) = (mat1 ** (mat2 ** mat3)).

Lemma 1.1.2 in arXiv:1012.5857v3
Lemma weighting_coweighting_sum {m n : nat} (mat : Matrix R m n)
(wei : weighting mat) (cowei : coweighting mat)
(assocax : matrix_mult_assoc_statement) :
Σ (pr1 wei) = Σ (pr1 cowei).
Proof.
apply (invmaponpathsweq weq_matrix_1_1).
intermediate_path ((row_vec (const_vec (1%rig))) ** (col_vec (pr1 wei))).
- apply sum_entries1.
- refine (!maponpaths (λ z, z ** _) (pr2 cowei) @ _).
refine (assocax _ _ _ _ _ _ _ @ _).
refine (maponpaths (λ z, _ ** z) (pr2 wei) @ _).
apply pathsinv0, sum_entries2 .
Defined.

Definition 1.1.3 in arXiv:1012.5857v3
Definition has_magnitude {n m : nat} (mat : Matrix R m n) : UU :=
(weighting mat) × (coweighting mat).

Definition magnitude {n m : nat} (m : Matrix R m n) (has : has_magnitude m) : R :=
Σ (pr1 (dirprod_pr1 has)).

End Weighting.