Library UniMath.Algebra.Matrix
Require Import UniMath.Foundations.PartA.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.Combinatorics.FiniteSequences.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.Algebra.IteratedBinaryOperations.
Require Import UniMath.Algebra.RigsAndRings.
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
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.
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.
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.
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.
Definition entrywise {X : UU} (n m : nat) (op : binop X) : binop (Matrix X n m) :=
λ mat1 mat2 i, pointwise _ op (mat1 i) (mat2 i).
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.
Structures
Matrix rig
Summation and pointwise multiplication
Local Notation Σ := (iterop_fun rigunel1 op1).
Local Notation "R1 ^ R2" := ((pointwise _ op2) R1 R2).
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).
{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).
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.
∑ 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.
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)).
∏ (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.
(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