-
Notifications
You must be signed in to change notification settings - Fork 0
/
unitary.v
173 lines (147 loc) · 5.34 KB
/
unitary.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
From mathcomp Require Import all_ssreflect all_algebra complex.
Require Import lens dpower.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Local Open Scope complex_scope.
Section unitary.
Variable R : rcfType.
Let C : comRingType := R[i].
Let Co : lmodType C := C^o.
Variable I : finType.
Variable dI : I.
Notation dpsquare n := (dpmatrix I C n n).
Notation id_dpmatrix := (id_dpmatrix I C).
Notation dpmatrixmx := (dpmatrixmx dI).
Notation mor := (mor I C).
Notation endo n := (mor n n).
Notation focus := (focus dI).
Local Notation "T '^^' n " := (dpower I n T).
Definition adjointmx n m (M : 'M[C]_(n,m)) := \matrix_(i,j) (M j i)^*.
Definition unitarymx n M := @adjointmx n n M *m M == 1%:M.
Lemma adjointmx_mul n m p (M : 'M[C]_(n,m)) (N : 'M[C]_(m,p)) :
adjointmx (M *m N) = adjointmx N *m adjointmx M.
Proof.
apply/matrixP => i j; rewrite !mxE.
rewrite rmorph_sum; apply eq_bigr => /= k _.
by rewrite !mxE -rmorphM /= mulrC.
Qed.
Lemma unitarymx_mul n (M N : 'M[C]_n) :
unitarymx M -> unitarymx N -> unitarymx (M *m N).
Proof.
move => /eqP UM /eqP UN; apply/eqP.
by rewrite adjointmx_mul mulmxA -(mulmxA (adjointmx N)) UM mulmx1.
Qed.
Section unitary_dpmatrix.
Variable n : nat.
Variable M : dpsquare n.
Definition dpadjoint m (N : dpmatrix I C m n) : dpmatrix I C n m :=
[ffun vi => [ffun vj => (N vj vi)^*]].
Definition dpunitary := dpadjoint M *d M == id_dpmatrix n.
Lemma dpadjointE m (N : dpmatrix I C m n) :
dpmatrixmx (dpadjoint N) = adjointmx (dpmatrixmx N).
Proof. apply/matrixP => i j; by rewrite !mxE !ffunE. Qed.
Lemma dpunitaryE : dpunitary = unitarymx (dpmatrixmx M).
Proof.
case/boolP: dpunitary => /eqP Hts; apply/esym/eqP.
- by rewrite -dpadjointE -dpmatrixmx_mul Hts dpmatrixmx_id.
- move=> Hmx; elim Hts.
rewrite -mxdpmatrix_id // -Hmx mxdpmatrix_mul //.
by rewrite -dpadjointE !dpmatrixmxK.
Qed.
Lemma unitary_invP : dpadjoint M = M ->
reflect (forall T, involutive (dpmor M T)) dpunitary.
Proof.
rewrite /dpunitary => ->.
apply: (iffP idP) => [/eqP|] Hinv.
- move=> T v.
move: (f_equal (fun M => dpmor M T v) Hinv).
by rewrite dpmor_comp -idmorE.
- apply/eqP.
rewrite -[LHS]dpmorK -[RHS]dpmorK.
apply mordp_eq => T v.
rewrite dpmor_comp -idmorE /=.
by have /= -> := Hinv T.
Qed.
End unitary_dpmatrix.
Lemma dpadjoint_mul n m p M N :
dpadjoint (M *d N) = @dpadjoint m p N *d @dpadjoint n m M.
Proof.
rewrite -[LHS](dpmatrixmxK dI) dpadjointE dpmatrixmx_mul.
by rewrite adjointmx_mul -!dpadjointE -dpmatrixmx_mul dpmatrixmxK.
Qed.
Lemma dpunitary_mul n (M N : dpsquare n) :
dpunitary M -> dpunitary N -> dpunitary (dpmul M N).
Proof. rewrite !dpunitaryE dpmatrixmx_mul; exact/unitarymx_mul. Qed.
Lemma unitarymxE n (M : 'M[C]_(#|I|^n)) :
unitarymx M = dpunitary (mxdpmatrix M).
Proof. by rewrite dpunitaryE mxdpmatrixK. Qed.
Section unitary_mor.
(* One could probably replace tinner by any bilinear form *)
Definition tinner n (s t : Co ^^ n) := \sum_i (s i)^* * (t i).
Definition unitary_mor m n (f : mor m n) :=
forall s t, tinner (f Co s) (f Co t) = tinner s t.
(* Actually this only makes sense for n >= m, since the rank must be at
least m to be unitary *)
Lemma idmorU n : unitary_mor (idmor I C n).
Proof. done. Qed.
Lemma unitary_morP n M :
reflect (@unitary_mor n n (dpmor M)) (dpunitary M).
Proof.
rewrite /dpunitary /unitary_mor.
apply/(iffP idP).
- move=> Uf s t; move/eqP: Uf.
move/(f_equal
(fun ts => dpmul (dpadjoint (curry0 _ s)) (dpmul ts (curry0 _ t)))).
rewrite !dpmulA -dpmulA -dpadjoint_mul mul1dp //.
move/(f_equal (fun M : dpsquare 0 => M [tuple] [tuple])).
rewrite !ffunE. under [RHS]eq_bigr do rewrite !ffunE.
move=> Uf; rewrite -{}[RHS]Uf.
apply eq_bigr => vi _; rewrite !ffunE !dpmorE.
by congr (_^* * _); apply eq_bigr => vj _; rewrite !ffunE.
- move=> Uf; apply/eqP/ffunP => vi; apply/ffunP => vj.
rewrite !ffunE; under eq_bigr do rewrite !ffunE.
have := Uf (dpbasis C vj) (dpbasis C vi).
rewrite /tinner.
under eq_bigr do rewrite !dpmorE !sum_dpbasisKo.
move ->.
under eq_bigr do rewrite !ffunE.
by rewrite sum_muleqr [LHS]conjc_nat eq_sym.
Qed.
Lemma unitary_comp m n p (f : mor n p) (g : mor m n) :
unitary_mor f -> unitary_mor g -> unitary_mor (f \v g).
Proof. move=> Hf Hg s t /=; by rewrite Hf. Qed.
Lemma unitary_focus n m (l : lens n m) (f : endo m) :
unitary_mor f -> unitary_mor (focus l f).
Proof.
rewrite /unitary_mor /tinner => /= Uf s t.
rewrite 2!(reindex_merge _ dI l) /=.
rewrite [LHS]exchange_big [RHS]exchange_big /=.
apply eq_bigr => vj _.
pose sel s : Co ^^ m := dpmap (dpsel vj) (curry dI l s).
transitivity (\sum_i (sel s i)^* * sel t i); last first.
apply eq_bigr => vi _; by rewrite !ffunE /dpsel !ffunE.
rewrite -Uf; apply eq_bigr => vi _.
rewrite focusE /=.
rewrite /uncurry !ffunE !extract_merge !extractC_merge.
by rewrite -!(morN f) !ffunE.
Qed.
End unitary_mor.
Section projection.
Variables (n m : nat) (l : lens n m).
Let norm p := fun s : Co ^^ p => (sqrtc (tinner s s) : Co).
Definition proj (t : Co ^^ n) : Co ^^ m :=
dpmap (@norm _) (curry dI l t).
Lemma proj_focusE p (l' : lens n p) (f : endo p) (t : Co ^^ n) :
[disjoint l & l'] -> unitary_mor f ->
proj (focus l' f Co t) = proj t.
Proof.
move=> Hdisj Uf.
rewrite /proj -(lmake_compE Hdisj) focus_others // uncurryK /=.
apply/ffunP => vi.
by rewrite !ffunE /norm unitary_focus.
Qed.
End projection.
End unitary.