-
Notifications
You must be signed in to change notification settings - Fork 3
/
eff.tex
8139 lines (8039 loc) · 303 KB
/
eff.tex
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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\chapter{Diamond, andthen, dagger}\label{chapter2}
\begin{parsec}{1730}%
\begin{point}{10}%
In the previous chapter and in \cite{bram}
we have studied categorical properties of von Neumann algebras.
In this chapter we change pace:
we study categories that resemble the
category of von Neumann algebras.
The goal of this line of study is to identify
axioms which uniquely pick out the category of von Neumann algebras.
We do not reach this ambitious goal ---
instead we will build up to a characterization of
the existence of a unique $\dagger$-structure
on the pure maps of a von Neumann algebras-like category.
\end{point}
\begin{point}{20}%
As a basic axiom we will require the categories we consider to be
effectuses (which will be defined in \sref{dfn-effectus}).
For us the definition of an effectus will play a similar role
to that of a topological space for a geometer.
In many applications,
general topological spaces on their own are of little interest:
the axioms are so weak that there are
many (for the application) pathological examples.
These weak axioms, however, are very expressive in the sense
that they allow for the definition of many useful notions.
Herein lies the strength of topological spaces ---
as a stepping stone:
many important classes of mathematical spaces
are just plain topological spaces with a few additional axioms.
Similarly, there will be many pathological effectuses.
Their use for us lies in their expressiveness.
\end{point}
\begin{point}{30}%
Before we dive into effectuses,
we need to learn about effect algebras (and related structures),
which were introduced by mathematical physicists as
a generalization of Boolean algebra to study fuzzy predicates
in quantum mechanics.
For us, effectuses are the
categorical counterpart of effect algebras.\footnote{Effect
algebroids~\cite{roumen,roumen2016cohomology} are a different
categorification with applications in cohomology.}
After this, we continue with a brief, but thorough development
of the basic theory of effectuses.
There is a lot more to say about effectuses
(see \cite{effintro}), which has been omitted
to avoid straining the reader.
We will indulge, however,
in one tangent,
which can be skipped:
the study of abstract convex sets in
\S\ref{more-aconvm}.
For the moment, think of an effectus as a generalization
of the opposite category of von Neumann algebras:
the objects represent the physical systems
(or data types, if you like)
and the maps represent the physical processes
(or properly typed programs).
\end{point}
\begin{point}{40}%
The first two axioms we add on top of those of an effectus
are the existence of quotients and comprehension.
It's helpful to discuss the origin of these axioms.
It started with the desire to axiomatize categorically
the sequential product on a von Neumann algebra~$\scrA$,
that is the operation~$\andthen{a}{b} \equiv \sqrt{a} b \sqrt{a}$,
which represents sequential measurement
of first~$a$ \emph{andthen} $b$.
The sequential product is a quantum mechanical generalization
of classical conjunction (logical `and').
In contrast to the tame~$\wedge$ in a Boolean algebras,
the sequential product does not obey a lot of insightful
formulas.
The sequential product as a binary operation
has received quite some attention \cite{gudder2008characterization,gheondea2004sequential,gudder2001sequential,li2011sequential,gudder2005open,shen2009not,gudder2005uniqueness,jun2009remarks,weihua2009uniqueness,tkadlec2008atomic,jia2010entropy,arias2004almost}.
We approach the sequential product in a rather different way:
we take a step back and
consider the map~$\asrt_a(b) \equiv \andthen{a}{b}$
for fixed~$a$. ($\asrt_a$ is named after the \texttt{assert} statement
used in many programming languages,
see~\sref{asrt-remarks}.)
This map~$\asrt_a$ factors in two:
\begin{equation*}
\xymatrix@C+2pc@R-2pc{
\scrA \ar[r]^\pi & \ceil{a} \scrA \ceil{a} \ar[r]^\xi
& \scrA \\
b \ar@{|->}[r] & \ceil{a}b\ceil{a}
\ar@{|->}[r] & \sqrt{a}b\sqrt{a}.
}
\end{equation*}
It turned out that both~$\pi$ and~$\xi$ have
nice and dual (in a sense) defining universal properties
which can be expressed in an effectus:
$\pi$ is a comprehension and~$\xi$ is a quotient.\footnote{%
Beware: an effectus quotient is not the same thing
as a von Neumann-algebra quotient.}
\end{point}
\begin{point}{50}%
The existence of quotients and comprehension in some effectus~$C$
is interesting on its own, but with
two additional axioms (the existence of images and
preservation of images under orthocomplementation),
we get a surprisingly firm handle
on the \emph{possibilistic} side of~$C$,
by means of the existence
of a certain functor~$(\ )_\diamond\colon C \to \mathsf{OMLat}$
to the category of orthomodular lattices.
In the guiding example of von Neumann algebras,
we have~$f_\diamond = g_\diamond$
if and only
there are no post-measurement~$a$ and initial state~$\omega$
that can determine with certainty
whether~$f$ or~$g$ has been performed.\footnote{%
In symbols: $
f_\diamond = g_\diamond \iff
\bigl(\forall a,\omega.\ \omega(f(a)) = 0 \ \Leftrightarrow\ \omega(g(a)) = 0\bigr).$}
With this functor we can introduce several
possibilistic notions of which~$\diamond$-adjoint
and~$\diamond$-positive are the most important.
Because of the central role of~$\diamond$,
we call an effectus with these axioms
a~$\diamond$-effectus.
\end{point}
\begin{point}{60}%
The axioms of a~$\diamond$-effectus do not force
any coherence between the quotients and comprehension.
This has been a roadblock to the axiomatization
of the sequential product for quite a while.
The key insight was the following:
the map~$\asrt_a$ (i.e.~$b\mapsto \andthen{a}{b}$)
is the unique~$\diamond$-positive map on~$\scrA$
with~$\asrt_a(1) = a$.
We turn this theorem into an axiom:
an~$\&$-effectus is
a~$\diamond$-effectus
where there are such unique~$\diamond$-positive maps~$\asrt_a$
and where an additional polar decomposition axiom holds.
In an~$\&$-effectus, the predicates on an object carry a canonical
binary operation~$\&$
which is the intended sequential product in
the case of von Neumann algebras.
\end{point}
\begin{point}{70}[pure-effectus]%
In an effectus, we call a map pure if it can be written
as the composition of quotients and comprehensions.
In~\sref{paschke-pure} we saw that in the case of von Neumann algebras,
a map is pure (in this sense) if and only if the corresponding Paschke
embedding is surjective.
In particular, the pure maps~$\scrB(\scrH) \to \scrB(\scrK)$
are exactly of the form~$\ad_v$
(for bounded operators~$v\colon \scrK \to \scrH$)
which carry a~$\dagger$-structure,
namely~$(\ad_v)^\dagger = \ad_{v^*}$.
This begs the question: can we define a~$\dagger$ on all pure maps
in an~$\&$-effectus?
The main result of this chapter
is Theorem~\sref{dagger-theorem},
which gives necessary and sufficient conditions
for an~$\&$-effectus
to have a well-behaved~$\dagger$-structure on its pure maps.
After this apogee,
we tie up some lose ends
and discuss how these
structures compare to those already known in the literature.
\end{point}
\end{parsec}
\section{Effect algebras and related structures}
\begin{parsec}{1740}%
\begin{point}{10}%
Before we turn to effectuses,
it is convenient to introduce some lesser-known algebraic structures
of which the effect algebra is the most important.
It will turn out that the set of predicates associated to an object in
an effectus can be arranged into an effect algebra.
In this way, effect algebras play the same role
for effectuses as Heyting algebras for toposes.
First, we will recall the definition of partial commutative monoid (PCM)
--- as later in \sref{cho-thm}
we will see that the partial maps between
two objects in an effectus can be arranged into a PCM.
\end{point}
\begin{point}{20}[dfn-pcm]{Definition}%
A \Define{partial commutative monoid} (\Define{PCM})~$M$
\index{PCM}
is a set~$M$ together with distinguished element~$0 \in M$
and a partial binary operation~$\ovee$ such that
for all~$a,b,c \in M$
--- writing~$a \perp b$ whenever~$a \ovee b$ is defined
--- we have
\begin{enumerate}
\item \emph{(partial commutativity)}
if $a \perp b$, then~$b \perp a$ and~$a \ovee b = b \ovee a$;
\item \emph{(partial associativity)}
if $a \perp b$ and~$a \ovee b \perp c$,
then~$b \perp c$, ~$a \perp b \ovee c$
and~$(a \ovee b) \ovee c = a \ovee (b \ovee c)$ \emph{and}
\item \emph{(zero)}
$0 \perp a$ and~$0 \ovee a = a$.
\end{enumerate}
A map~$f\colon M \to N$
between PCMs~$M$ and~$N$
is called an \Define{PCM homomorphism}
\index{PCM!homomorphism}
if for all~$a, b \in E$
with~$a \perp b$,
we have~$f(a) \perp f(b)$
and~$f(a) \ovee f(b) = f(a \ovee b)$.
Write~$\Define{\textsf{PCM}}$ for the category
\index{\textsf{PCM}}
of PCMs with these homomorphisms. (Cf.~\cite{corefl,Wehrung2017})
For~$a,b$ in a PCM~$M$,
we say~$\Define{a \leq b}$
\index{*leq@$\leq$!in PCM/EA}
iff~$a \ovee c = b$ for some~$c \in M$.
\end{point}
\begin{point}{30}[pcm-preorder]{Exercise}%
Show a PCM is preordered by~$\leq$.
\end{point}
\begin{point}{40}%
The partial commutativity and associativity of a PCM
ensure that a sum only depends on which elements
occur (and how often), instead of their order.
Formally:
if~$(\cdots( x_1 \ovee x_2) \ovee \cdots) \ovee x_n$
exists some~$x_1, \ldots, x_n$ in some PCM, then so
does~$(\cdots( x_{\pi(1)} \ovee x_{\pi(2)}) \ovee \cdots) \ovee x_{\pi(n)}$
for any permutation~$\pi$ of~$\{1,\ldots,n\}$ and
\begin{equation*}
(\cdots( x_1 \ovee x_2) \ovee \cdots) \ovee x_n
\ = \ (\cdots( x_{\pi(1)} \ovee x_{\pi(2)}) \ovee \cdots) \ovee x_{\pi(n)}.
\end{equation*}
Thus parantheses are superfluous and we will often leave them out:
\begin{equation*}
\bigovee^n_{i=1} x_i \ \equiv \ \Define{x_1 \ovee \cdots \ovee x_n}
\ \equiv\
(\cdots( x_1 \ovee x_2) \ovee \cdots) \ovee x_n.
\end{equation*}
\end{point}
\spacingfix{}
\end{parsec}
\begin{parsec}{1750}%
\begin{point}{10}[dfn-ea]{Definition}%
A PCM~$E$ together with distinguished element~$1 \in E$
is called an \Define{effect algebra} (\Define{EA}) \cite{ea}
\index{EA}
\index{effect algebra}
provided that
\begin{enumerate}
\item
\emph{(orthocomplement)}
for every~$a$
there is a unique~$\Define{a^\perp}$
\index{orthocomplement!in an effect algebra}
\index{*perp@$(\ )^\perp$!element effect algebra}
with~$a \ovee a^\perp = 1$ \emph{and}
\item
\emph{(zero--one)}
if~$a \perp 1$, then~$a = 0$.
\end{enumerate}
A map~$f\colon E \to F$
between effect algebras~$E$ and~$F$
is called an \Define{effect algebra homomorphism}
\index{effect algebra!homomorphism}
if it is a PCM homomorphism that preserves~$1$;
concretely:
\begin{enumerate}
\item \emph{(additive)}
$a \perp b$ implies $f(a) \perp f(b)$ and~$f(a)\ovee f(b) = f(a\ovee b)$
\emph{and}
\item \emph{(unital)}
$f(1) = 1$.
\end{enumerate}
(It follows that~$f(0)=0$ and~$f(a^\perp) = f(a)^\perp$. See~\sref{exc-eamorphism}.)
Write~$\Define{\textsf{EA}}$
\index{\textsf{EA}}
for the category
of effect algebras with these homomorphisms.
A subset~$D \subseteq E$ is a \Define{sub-effect algebra}
\index{effect algebra!sub-} of~$E$
if~$0,1 \in D$ and for any~$a,b \in D$
with~$a\perp b$, we have~$a \ovee b \in D$
and~$a^\perp \in D$.
\end{point}
\begin{point}{20}[eaexamples]{Examples}%
There are many examples of effect algebras
--- we only give a few.
\begin{enumerate}
\item
The unit interval
$[0,1]$ with partial addition is an effect algebra ---
i.e.:~$x \perp y$
whenever~$x +y \leq 1$ and then $x \ovee y = x + y$,
$x^\perp = 1-x$.
\item
Generalizing the previous:
if~$G$ is an ordered group
with distinguished element~$1$,
then the order interval~$[0,1]_G \equiv \{x;\ x\in G;\ 0 \leq x\leq 1\}$
is an effect algebra
with~$x \perp y$ whenever~$x +y \leq 1$;
$x \ovee y = x + y$ and~$x^\perp = 1-x$.
\item
In particular,
if~$\scrA$ is any von Neumann algebra,
then the set of \Define{effects}~$[0,1]_\scrA$
\index{effects}
\index{*01@$[0,1]_\scrA$}
forms an effect algebra
with~$a \perp b$ whenever~$a +b \leq 1$;
$a \ovee b = a + b$ and~$a^\perp = 1-a$.
The `effect' in effect algebra originates from this example.
\item
Any orthomodular lattice~$L$ (defined in \sref{dfn-orthomodular-lattice})
is an effect algebra
with the same orthocomplement,
$x \perp y$ whenever~$x \leq y^\perp$
and~$x \ovee y = x \vee y$. (See e.g.~\cite[prop.~27]{basmsc}.)
\item
In particular,
any Boolean algebra~$L$
is an effect algebra
with complement as orthocomplement,
~$x \perp y$ whenever~$x \wedge y = 0$ and
$x \ovee y = x \vee y $.
\item
The one-element Boolean algebra~$1 \equiv \{0=1\}$
is the final object in \textsf{EA}
and the two-element Boolean algebra~$2 \equiv \{0,1\}$
is the initial object in \textsf{EA}.
\end{enumerate}
\spacingfix{}
\end{point}
\begin{point}{30}[ea-product]{Exercise}%
Let~$E$ and~$F$ be effect algebras.
First show that the cartesian product~$E \times F$
is an effect algebra with componentwise operations.
Show that this is in fact the categorical product of~$E$ and~$F$
in \textsf{EA}.
(The category \textsf{EA} is in fact complete and cocomplete;
for this and more categorical properties,
see \cite{corefl}.)
\end{point}
\begin{point}{40}[ea-redund]{Exercise}%
There is a small redundancy in our definition of effect algebra:
show that the zero axiom ($x \ovee 0 = x$)
follows from the remaining axioms (partial commutativity,
partial associativity, orthocomplement and zero--one.)
\end{point}
\begin{point}{50}[eabasics]{Proposition}%
In any effect algebra~$E$ with~$a,b,c\in E$, we have
\begin{enumerate}
\item \emph{(involution)}
$a^{\perp\perp} = a$;
\item
$1^\perp= 0$ and~$0^\perp = 1$;
\item \emph{(positivity)}
if~$a\ovee b = 0$, then~$a = b= 0$;
\item \emph{(cancellation)}
if~$a\ovee c = b\ovee c$, then~$a = b$;
\item the relation $\leq$ (from \sref{dfn-pcm}) partially orders~$E$;
\item $a \leq b$ if and only if $b^\perp \leq a^\perp$;
\item if~$a \leq b$ and~$b \perp c$, then~$a \perp c$
and~$a \ovee c \leq b \ovee c$ \emph{and}
\item $a \perp b$ if and only if~$a \leq b^\perp$.
\end{enumerate}
\spacingfix{}
\begin{point}{60}{Proof}%
(These proofs are well-known,
see for instance~\cite{dvurecenskij2013new}.)
By partial commutativity and definition
of orthocomplement both~$a^\perp \ovee a = 1$
and~$a^\perp \ovee a^{\perp\perp} = 1$.
So by uniqueness of orthocomplement,
we must have~$a= a^{\perp\perp}$, which is point 1.
Clearly~$0 \ovee 1 = 1$,
so~$1^\perp = 0$ and~$0^\perp = 1$,
which is point 2.
For point 3, assume~$a \ovee b = 0$.
Then~$a \ovee b \perp 1$
and so by partial associativity~$b \perp 1$.
By zero--one, we get~$b = 0$.
Similarly~$a=0$, which shows point 3.
For point 4, assume~$ a \ovee c = b \ovee c$.
From partial associativity and commutativity, we get
$ ((a \ovee b)^\perp\ovee a) \ovee c =
((a \ovee b)^\perp\ovee a) \ovee b = 1$
and so by uniqueness of
orthocomplement~$c = ((a\ovee b)^\perp\ovee a)^\perp = b$,
which is point~4.
By \sref{pcm-preorder},
we only need to show that~$\leq$ is antisymmetric
for point~5.
So assume~$a \leq b$ and~$b \leq a$
for some~$a,b\in E$.
Pick~$c,d \in E$ with~$a \ovee c = b$ and~$b \ovee d = a$.
Then~$a = (a \ovee c) \ovee d = a \ovee (c \ovee d)$.
By cancellation~$c \ovee d = 0$.
So by positivity~$c = d= 0$.
Hence~$a = b$.
For point 6, assume~$a\leq b$.
Pick~$c \in E$ with~$a \ovee c = b$.
Clearly~$a \ovee a^\perp = 1 = b \ovee b^\perp = a \ovee c \ovee b^\perp$,
so by cancellation~$a^\perp = c \ovee b^\perp$,
which is to say~$b^\perp \leq a^\perp$.
For point 7, assume~$a \leq b$ and~$b \perp c$.
Pick~$d$ with~$a \ovee d = b$.
By partial associativity and commutativity
we have~$b \ovee c = (a \ovee d) \ovee c = (a \ovee c) \ovee d$,
so~$a \perp c$ and~$a \ovee c \leq b \ovee c$.
For point 8, first assume~$a \perp b$.
Then~$a \ovee b \ovee (a \ovee b)^\perp = 1 = b \ovee b^\perp$.
So by cancellation~$b^\perp = a \ovee (a \ovee b)^\perp$,
hence~$a \leq b^\perp$.
For the converse, assume~$a \leq b^\perp$.
Then~$a \ovee c = b^\perp$ for some~$c$.
Hence~$a \ovee c \perp b$
and so by partial associativity and commutativity,
we get~$a \perp b$, as desired.
\qed
\end{point}
\end{point}
\end{parsec}%
\begin{parsec}{1760}%
\begin{point}{10}{Definition}%
Suppose~$E$ is an effect algebra.
Write~$\Define{b \ominus a}$
\index{*ominus@$\ominus$}
for the (by cancellation) unique element (if it exists)
with~$a \ovee (b \ominus a) = b$.
\end{point}
\begin{point}{20}[exc-dposet]{Exercise*}%
Show that for any effect algebra~$E$, we have
\begin{enumerate}
\item[(D1)]~$a \ominus b$ is defined if and only if~$b \leq a$;
\item[(D2)]~$a \ominus b \leq a$ (if defined);
\item[(D3)]~$a \ominus (a \ominus b) = b$ (if defined) \emph{and}
\item[(D4)]~if $a \leq b \leq c $,
then~$c \ominus b \leq c \ominus a$
and~$(c \ominus a) \ominus (c \ominus b) = b \ominus a$.
\end{enumerate}
\spacingfix{}
\begin{point}{30}%
Let~$E$ be a poset with maximum element~$1$
and partial binary operation~$\ominus$
satisfying~(D1)--(D4).
Define~$a \ovee b = c \Leftrightarrow c \ominus b = a$
and~$a^\perp = 1 \ominus a$.
Show that this turns~$E$ into an effect algebra
with compatible order and~$\ominus$.
\end{point}
\begin{point}{40}{Remark}%
Such a structure~$(E,\ominus,1)$ is called a \Define{difference-poset}
\index{D-poset}
(\Define{D-poset}) \cite{kopka1994d} and is, as we have just seen,
an alternative way to axiomatize effect algebras.
\end{point}
\end{point}
\begin{point}{50}[exc-eamorphism]{Exercise}%
Show that for an effect algebra homomorphism~$f\colon E \to F$,
we have
\begin{enumerate}
\item~\emph{(preserves zero)} $f(0) = 0$;
\item~\emph{(order preserving)} if $a \leq b$, then~$f(a) \leq f(b)$;
\item~if~$a\ominus b$ is defined,
then $f(a \ominus b) = f(a) \ominus f(b)$ \emph{and}
\item consequently~$f(a^\perp) = f(a)^\perp$.
\end{enumerate}
\spacingfix{}
\end{point}
\end{parsec}
\begin{parsec}{1770}%
\begin{point}{10}%
For real numbers we have~$a + b = \min \{a,b\} + \max \{a, b\}$.
The following is a generalization to effect algebras.
\end{point}
\begin{point}{11}[ea-modularity-prop]{Proposition}%
Suppose~$E$ is an effect algebra.
If the infimum~$a \wedge b$
exists for some~$a,b \in E$ with~$a \perp b$,
then their supremum~$a \vee b$ exists as well and
\begin{equation*}
a \ovee b \ = \ (a \wedge b) \,\ovee\, (a \vee b).
\end{equation*}
\spacingfix{}
\begin{point}{20}[modularity-lemma-proof]{Proof}%
(This result appeared in my master's thesis~\cite[prop.~15]{basmsc}.
It turns out that it was already proven before
(in D-poset form) \cite[prop.~1.8.2]{dvurecenskij2013new}.)
The result follows from this lemma:
if~$(x \ominus c) \wedge (x \ominus d)$ exists,
then~$c \vee d$ exists as well
and~$(x \ominus c) \wedge (x \ominus d)
= x \ominus (c \vee d)$.
Indeed:
\begin{equation*}
a \wedge b \ = \
((a \ovee b) \ominus a) \wedge ((a \ovee b) \ominus b) \ = \
(a \ovee b) \ominus (a \vee b)
\end{equation*}
and so~$(a \wedge b) \ovee (a \vee b) = a \ovee b$, as desired.
\begin{point}{30}%
Now, we prove the lemma.
Assume~$(x \ominus c) \wedge (x \ominus d)$ exists.
Note~$x \ominus c = (x^\perp \ovee c)^\perp$.
As~$z \mapsto z^\perp$ is an order anti-isomorphism,
we see~$(x^\perp \ovee c) \vee (x^\perp \ovee d)$
exists and~$(x^\perp \ovee c) \vee (x^\perp \ovee d)
= ((x \ominus c)\wedge (x \ominus d))^\perp$.
Clearly~$ (x^\perp \ovee c) \vee
(x^\perp \ovee d) \geq x^\perp$.
Write~$r := ((x^\perp \ovee c) \vee
(x^\perp \ovee d)) \ominus x^\perp$.
We will show~$r = c \vee d$.
It is easy to see~$r \geq c$ and~$r \geq d$.
Assume~$s$ is any element with~$s \geq c$ and~$s \geq d$.
Note~$x^\perp \ovee s \geq x^\perp \ovee c$
and~$x^\perp \ovee s \geq x^\perp \ovee d$,
hence~$x^\perp \ovee s \geq (x^\perp \ovee c) \vee (x^\perp \ovee d)$
and so~$ s \geq r$.
We have shown~$r = c \vee d$.
Consequently~$ (x \ominus c)\wedge (x \ominus d)
= ((x^\perp \ovee c) \vee (x^\perp \ovee d))^\perp
= (r \ovee x^\perp)^\perp =
x \ominus (c \vee d) $, as promised. \qed
\end{point}
\end{point}
\end{point}
\begin{point}{40}[dfn-orthomodular-lattice]{Definition}%
An \Define{ortholattice}~$L$
\index{ortholattice}
is a bounded lattice with orthocomplement
--- that is: it has a minimum~$0$,
a maximum~$1$
and a unary operation~$(\ )^\perp$
satisfying
\begin{multicols}{2}
\begin{enumerate}
\item $a \wedge a^\perp = 0$;
\item $a \vee a^\perp = 1$;
\item $a \leq b \ \Rightarrow\ b^\perp \leq a^\perp$ and
\item $a^{\perp\perp} = a$.
\end{enumerate}
\end{multicols}
\noindent An ortholattice is \Define{orthomodular}\index{orthomodular!lattice}
provided
\begin{equation*}
a \ \leq \ b \quad \implies \quad a \vee (a^\perp \wedge b) \ =\ b.
\end{equation*}
See, for instance~\cite{kalmbach1983orthomodular,dvurecenskij2013new,birkhoff1936logic}.
\end{point}
\begin{point}{50}{Example}%
The lattice of projections in a von Neumann algebra
is an orthomodular lattice with
orthocomplement~$p^\perp \equiv 1 - p$.
\end{point}
\begin{point}{60}[orth-ea-is-orthomodular]{Proposition}%
An effect algebra~$E$
that is an ortholattice
is also orthomodular.
\begin{point}{70}{Proof}%
(For a different proof, see \cite[prop.~1.5.8]{dvurecenskij2013new}.)
Assume~$a \leq b$.
We have to show~$a \vee (a^\perp \wedge b) = b$.
Note~$a \wedge (a^\perp \wedge b) \leq a \wedge a^\perp = 0$
and so by \sref{ea-modularity-prop}
we have~$a \vee (a^\perp \wedge b) = a \ovee (a^\perp \wedge b)$.
Thus it is sufficient to prove~$a^\perp \wedge b = b \ominus a$.
Note~$a^\perp = (b \ominus a) \ovee b^\perp$
and~$b = (b \ominus a) \ovee a$.
Similar to~\sref{modularity-lemma-proof}
one can show that
\begin{equation*}
(b \ominus a) \ovee (b^\perp \wedge a)
\ = \
((b \ominus a) \ovee b^\perp) \wedge
((b \ominus a) \ovee a) \ \equiv \ a^\perp \ovee b,
\end{equation*}
but~$b^\perp \wedge a \leq b^\perp \wedge b = 0$
and so~$a^\perp \ovee b = b\ominus a$, as desired.
\qed
\end{point}
\end{point}
\end{parsec}
\subsection{Effect monoids}
\begin{parsec}{1780}%
\begin{point}{10}%
In \sref{dfn-mandso} we will see that the scalars of an effectus
form an effect monoid:
\end{point}
\begin{point}{20}[dfn-effect-monoid]{Definition}%
An \Define{effect monoid}~$M$ \cite{probdistrconv}
\index{effect monoid}
\index{*odot@$\odot$!effect monoid}
is an effect algebra
together with a binary operation~$\odot$
such that for all~$a,b,c,d \in M$, we have
\begin{enumerate}
\item \emph{(unit)}
$1 \odot a = a \odot 1 = a$;
\item \emph{(associativity)}
$(a \odot b) \odot c
=a \odot (b \odot c)$ \emph{and}
\item \emph{(distributivity)}
if~$a \perp b$ and~$c \perp d$,
then the following sum exists and
furthermore~$(a \odot c) \ovee (b \odot c) \ovee
(a \odot d) \ovee (b \odot d) = (a \ovee b) \odot (c \ovee d)$.
\end{enumerate}
(Phrased categorically:
an effect monoid is a monoid in \textsf{EA}
with the obvious tensor product
that relates bimorphisms to morphisms,
see~\cite{corefl,probdistrconv}.)
An effect monoid~$M$ is said to be \Define{commutative}
\index{effect monoid!commutative}
if we have~$a\odot b = b\odot a$ for all~$a,b \in M$.
A map~$f\colon M \to N$ between effect monoids
is called an \Define{effect monoid homomorphism}
\index{effect monoid!homomorphism}
if it is an effect algebra homomorphism
and furthermore~$f(a \odot b) = f(a) \odot f(b)$
for all~$a,b \in M$.
\end{point}
\begin{point}{30}[eff-monoid-examples]{Examples}%
Effect monoids are less abundant than effect algebras.
\begin{enumerate}
\item The effect algebra~$[0,1]$
is a commutative effect monoid with the usual product.
(This is the only way to turn~$[0,1]$ into an effect monoid
\cite[prop.~41]{basmsc}.)
\item We saw earlier that every Boolean algebra is an effect algebra
with~$x \ovee y = x \vee y$ defined iff~$x \wedge y = 0$.
The Boolean algebra is turned into an effect monoid
with~$x \odot y \equiv x \wedge y$.
In fact, every finite (not necessarily commutative) effect monoid
is of this form \cite[prop.~40]{basmsc} and thus commutative.
\item
In particular: the two-element Boolean algebra~$2 = {0,1}$
from~\sref{eaexamples}
is an effect monoid
with~$x \odot y = x \wedge y$.
\item There is a non-commutative effect monoid
based on the lexicographically ordered vector space~$\R^5$,
see ~\cite[cor.~51]{basmsc}.
\item Let~$M$ be an effect monoid.
Write~$M^{\mathsf{op}}$
for the effect monoid~$M$ with the opposite multiplication
--- that is: $a \odot_M b = b \odot_{M^\mathsf{op}} a$.
\end{enumerate}
\spacingfix{}
\end{point}
\begin{point}{31}[exc-emonzero]{Exercise}%
Show that~$a \odot 0 = a = 0 \odot a$
for any~$a$ in an effect monoid~$M$.
\begin{point}{40}%
Later, in a tangent,
we will need the following specific fact about effect monoids.
\end{point}
\end{point}
\begin{point}{50}[emond-lemma-for-conv]{Exercise}%
Assume~$M$ is an effect monoid
with~$a_1, \ldots, a_n, b_1, \ldots, b_n \in M$
such that~$\bigovee_i a_i = 1$
and~$\bigovee_i a_i \odot b_i = 1$.
Prove~$a_i \odot b_i = a_i$ for every~$1 \leq i \leq n$.
\end{point}
\end{parsec}
\subsection{Effect modules}
\begin{parsec}{1790}%
\begin{point}{10}%
We will see that in an effectus,
the effect monoid of scalars will act on
every effect algebra of predicates,
turning them into effect modules (see \sref{dfn-mandso}):
\end{point}
\begin{point}{20}[dfn-effect-module]{Definition}%
Suppose~$M$ is an effect monoid.
An \Define{effect module} $E$ over~$M$ \cite{corefl}
\index{effect module}
is an effect algebra together with an operation
$M \times E \to E$
denoted by~$(\lambda, a) \mapsto \lambda \cdot a$
such that for all~$a,b \in E$ and~$\lambda,\mu \in M$, we have
\begin{enumerate}
\item
$(\lambda \odot \mu) \cdot a = \lambda \cdot (\mu \cdot a)$;
\item
if~$a \perp b$,
then~$\lambda \odot a \perp \lambda \odot b$
and~$(\lambda \odot a) \ovee (\lambda\odot b) = \lambda \odot(a \ovee b)$;
\item
if~$\lambda \perp \mu$,
then~$\lambda \odot a \perp \mu \odot a$
and~$(\lambda \odot a) \ovee (\mu \odot a) = (\lambda \ovee \mu) \odot a$
\emph{and}
\item
$1 \odot a = a$.
\end{enumerate}
(Categorically: an effect module over~$M$
is an~$M$-action.)
An effect algebra homomorphism~$f\colon E \to F$
between effect modules over~$M$
is an $M$-\Define{effect module homomorphism}
\index{effect module!homomorphism}
provided~$\lambda \cdot f(a) = f(\lambda \cdot a)$
for all~$\lambda \in M$ and~$a \in E$.
Write~$\Define{\mathsf{EMod}_M}$
\index{$\mathsf{EMod}_M$}
for the category of effect modules over~$M$
with effect module homomorphisms between them.
\end{point}
\begin{point}{30}{Examples}%
There are many effect modules.
\begin{enumerate}
\item
Every effect algebra is an effect module over
the two-element effect monoid~$2$.
(In fact $\mathsf{EA} \cong \mathsf{EMod}_{2}$.)
The only effect module up-to-isomorphism over the one-element effect monoid~$1$
is the one-element effect algebra~$1$ itself.
\item
Effect modules over~$[0,1]$
are the same thing as
\Define{convex effect algebras},
see \cite{gudder1998representation,gudder1999convex}.
\index{effect algebra!convex}
If~$V$ is an ordered real vector space with order unit~$u$,
then~$[0,u]$ is an effect module over~$[0,1]$.
In fact, every effect module over~$[0,1]$
is of this form \cite{gudder1998representation}.
See also \cite[thm.~3]{jacobs2016expectation}
for the stronger categorical equivalence.
\end{enumerate}
\spacingfix{}
\end{point}
\end{parsec}
\section{Effectuses}
An effectus comes in two guises:
axiomatizing either a category of total maps
or a category of partial maps.
We will start off with the total form as it has the simplest axioms.
Later we will prefer to work with the partial form.
\begin{parsec}{1800}%
\begin{point}{10}[dfn-effectus]{Definition}%
A category $C$ is said to be an \Define{effectus in total form}
\index{effectus!in total form}
\cite{effintro,newdirections,statesofconvexsets}
if
\begin{enumerate}
\item $C$ has finite coproducts (hence an initial object~$0$)
and a final object~$1$;
\item all diagrams of the following
\index{kappa@$\kappa_i$, coprojection}
\index{$[\,\cdot\,,\,\cdot\,]$!cotupling}
\index{*bang@$"!$, initial/final map}
form\footnote{%
We write~$\Define{\kappa_i}$ for coproduct coprojections;
square brackets~$\Define{[f,g]}$ for coproduct cotupling;
$\Define{h+k} = [\kappa_1 \after h, \kappa_2 \after k]$
and~$\Define{!}$ for the unique maps associated to
either the final object~$1$ or initial object~$0$.} are pullbacks
\begin{equation}\label{pullbacks}
\vcenter{\xymatrix{
X+Y \ar[r]^{\id+{!}} \ar[d]_{!+\id} & X+1\ar[d]^{!+\id} \\
1+Y\ar[r]_{\id+!} & 1+1
}}
\qquad\qquad
\vcenter{\xymatrix{
X \ar[r]^{!} \ar[d]_{\kappa_1} & 1 \ar[d]^{\kappa_1} \\
X+Y\ar[r]_{{!}+{!}} & 1+1
}}
\end{equation}
\item\label{eff-joint-monicity} and the following two arrows are jointly monic.
\begin{equation*}
\xymatrix@C+2pc {
1+1+1 \ar@/^/[r]^{[\kappa_1,\kappa_2,\kappa_2]}
\ar@/_/[r]_{[\kappa_2,\kappa_1,\kappa_2]} & 1+1
}
\end{equation*}
\end{enumerate}
An arrow~$f\colon X \to Y+1$ is called a \Define{partial map} and written
\index{partial map}
$f\colon \Define{X \pto Y}$.
\index{*pto@$\pto$}
\begin{point}{20}%
One with an interest in physics might think of the objects
of an effectus as physical systems and its arrows as
the physical operations between them.
The final object~$1$ is the physical system with a single state.
The coproduct~$X+Y$ is the system that can be prepared as either~$X$ or as~$Y$.
An arrow~$1 \to X$ corresponds to a physical preparation of the system~$X$
and an arrow~$X \to 1+1$ is a yes--no measurement.
\end{point}
\begin{point}{30}%
In this sense an effectus can be seen as a generalized
probabilistic theory
--- not unlike the operational-probabilistic theories (OPT)
of Chiribella et al \cite{chiribella2010probabilistic}.
There are differences:
for instance, OPTs are equipped with a parallel composition of systems,
effectuses are not and OPTs always have the unit interval as scalars,
effectuses might not.
In \cite{tull2016operational} Tull compares effectuses and OPTs.
There are other approaches to categorical probabilistic theories;
see, for instance~\cite{wilceshortcut,gogioso2017categorical}.
\end{point}
\begin{point}{40}%
Studying programming languages, one would do better thinking of
the objects of an effectus as data types and
its arrows as the allowed operations between them (semantics of programs).
The final object~$1$ is the unit data type.
The coproduct~$X + Y$ is the union data type of~$X$ and~$Y$.
An arrow~$1 \to X$ is a value of~$X$
and an arrow~$X \to 1+1$ is a predicate on~$X$.
\end{point}
\begin{point}{50}[effectus-vn]%
Our main example of an effectus in total form
is the category~$\op{\vN}$\index{vN@$\vN$}
of von Neumann algebras with completely positive normal unital
maps in the opposite direction.
(To see~$\op\vN$ is an effectus in total form,
adapt the proof of \sref{emod-effectus}.)
The partial maps correspond to
ncp-maps~$f$ with~$f(1) \leq 1$.
(Equivalently: contractive ncp-maps.)
Some other examples appear later on in
\sref{emod-effectus}, \sref{exc-dm-effectus},
\sref{aconvm-is-effectus} and~\sref{effexamplesintro}.
For a comprehensive list of examples, see~\cite{effintro}.
\end{point}
\begin{point}{60}%
Let~$C$ be an effectus in total form.
Given two arrows~$f\colon X \to Y+1$
and~$g \colon Y \to Z+1$ (i.e.~partial maps~$X \pto Y$ and~$Y \pto Z$)
their composition as partial maps
is defined as~$g \hafter f \equiv [g, \kappa_2] \after f$.
Write~$\Define{\Par C}$ for the \Define{category of partial maps},
\index{ParC@$\Par C$}
which has the same objects
as~$C$, but as arrows~$X \to Y$ in~$\Par C$
we take arrows of the form~$X \to Y+1$ in~$C$,
which we compose using~$\hafter$
and with identity on~$X$ in~$\Par C$
given by~$\kappa_1 \colon X \to X+1$.\footnote{In categorical
parlance: $\Par C$ is the Kleisli category of
the monad~$(\ )+1\colon C \to C$.}
The category~$\Par C$ is not an effectus in total form --- instead it
is an effectus \emph{in partial form}.
\end{point}
\end{point}
\begin{point}{70}[effectus-in-partial-form]{Definition}%
A category~$C$ is called an \Define{effectus in partial form}
\index{effectus!in partial form}
\cite{effintro,kentapartial} if
\begin{enumerate}
\item
$C$ is a finPAC\footnote{Finitarily partially additive category.} \cite{kentapartial} (cf.~\cite{arbib}) --- that is:
\begin{enumerate}
\item
$C$ has finite coproducts $(+,0)$;
\item $C$ is $\mathsf{PCM}$-enriched --- that is:
\begin{enumerate}
\item
every homset $C(X,Y)$ has a partial binary operation~$\ovee$
and distinguished element~$0 \in C(X,Y)$
that turns~$C(X,Y)$ into a partial commutative monoid,
see \sref{dfn-pcm};
\item
if $f \perp g$ then both
$(h \after f) \perp (h \after g)$ and
$(f \after k) \perp (g \after k)$ \emph{and}
\begin{equation*}
h \after (f \ovee g) =
(h \after f) \ovee (h \ovee g)\qquad
(f \ovee g) \after k =
(f \after k) \ovee (g \after k)
\end{equation*}
for any~$f,g \colon X \to Y$,
$h\colon Y \to Y'$
and~$k \colon X'\to X$ \emph{and}
\item
\emph{(zero)}
$0 \after f = 0$ and $f \after 0 = 0$ for
any~$f\colon X \to Y$ \emph{and}
\end{enumerate}
\item
\emph{(compatible sum)}
for any~$b\colon X \to Y + Y$ we have
$\pproj_1 \after b \perp \pproj_2 \after b$,
where~$\Define{\pproj_i}\colon Y + Y \to Y$
\index{*pproj@$\pproj_i$}
are \Define{partial projectors}\footnote{%
Later, in~\sref{coprod-prod},
we will use the more slightly more general
${\pproj_1}\colon X_1 + X_2 \to X_1$ and
${\pproj_2}\colon X_1 + X_2 \to X_2$
defined by~$\pproj_1 = [\id,0]$
and~$\pproj_2 = [0,\id]$.} defined
\index{partial projectors}
by~$\pproj_1 \equiv [\id, 0]$
and~$\pproj_2 \equiv [0, \id]$ \emph{and}
\item
\emph{(untying)} if~$f\perp g$,
then~$\kappa_1\after f \perp \kappa_2 \after g$,
where~$\kappa_1$ and~$\kappa_2$ are coprojections
on the same coproduct
\emph{and}
\end{enumerate}
\item it has effects --- that is: there is a distinguished object~$I$
such that
\begin{enumerate}
\item for each object~$X$, the PCM~$C(X,I) \equiv \Define{\Pred X}$
\index{predX@$\Pred X$}
is an effect algebra, see \sref{dfn-ea}
--- in particular~$C(X,I)$
has a maximum element~$1$;
\item if~$1 \after f \perp 1 \after g$,
then~$f \perp g$ \emph{and}
\item if~$1 \after f = 0$, then~$f = 0$.
\end{enumerate}
\end{enumerate}
In this setting,
a map~$f\colon X \to Y$ is called \Define{total} if~$1 \after f = 1$.
\index{total map}
\begin{point}{80}{Remark}%
The untying and zero axioms are redundant: they follows from the others.
We include them, as they are part of the definition of finPAC.
\end{point}
\begin{point}{90}%
At first glance an effectus in partial form seems
to have a much richer structure than an effectus in total form.
This is not the case ---
effectuses in total and partial form are two views
on the same thing \cite{kentapartial,effintro}:
\end{point}
\end{point}
\begin{point}{100}[cho-thm]{Theorem (Cho)}%
Let~$C$ be an effectus in total form
and~$D$ be an effectus in partial form.
\begin{enumerate}
\item
The category~$\Par C$ is an effectus in partial form
with~$I = 1$.
\item
The total maps of~$D$ form an effectus in total form~$\Tot D$.
\item
Nothing is lost:
$\Par (\Tot D) \cong D$ and~$\Tot (\Par C )\cong C$.
\end{enumerate}
\spacingfix{}
\begin{point}{110}%
(The result can be rephrased categorically as
a 2-equivalence of the 2-category
of effectuses in partial form and
the 2-category of effectuses in total form.
For the details, see~\cite[\S5]{kentapartial}.)
To prove the Theorem
(in \sref{proof-cho-thm}),
we need some preparation.
\end{point}
\end{point}
\end{parsec}
\subsection{From partial to total}
\begin{parsec}{1810}%
\begin{point}{10}%
We will first show that the subcategory of
total maps of an effectus in partial form
is an effectus in total form.
This proof and especially the demonstration
that the squares in \eqref{pullbacks} are pullbacks,
will elucidate the axioms of an effectus in total form
and will make the proof in the opposite direction more palatable.
\end{point}
\begin{point}{20}[coproj-total]{Lemma}%
In an effectus in partial form,
coprojections are total.
\begin{point}{30}{Proof}%
(For the original and different proof see \cite[lem.~4.7(5)]{kentapartial}.)
Let~$\kappa_1 \colon X \to X+Y$ be any coprojection.
We have to show~$1 \after \kappa_1 = 1$.
Note that the first~$1$ denotes the maximum of~$\Pred X+Y$
and the second the maximum of~$\Pred X$.
Hence~$1_X = 1_X \after \id_X = (1_X \after [\id_X, 0]) \after \kappa_1
\leq 1_{X+Y} \after \kappa_1 \leq 1_X$.
Indeed~$1 \after \kappa_1 = 1$. \qed
\end{point}
\end{point}
\begin{point}{40}[cotupl-pcm]{Proposition}%
In an effectus in partial form,