-
Notifications
You must be signed in to change notification settings - Fork 23
/
choicefin.tex
355 lines (298 loc) · 14 KB
/
choicefin.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
\section{Choice for finite sets\titledagger}
\label{sec:choicefin}
This section is a short overview of how group theory is involved in
relating different choice principles for families of finite sets. A
paradigmatic case is that if we have choice for all families of
$2$-element sets, then we have choice for all families of $4$-element
sets.%
\footnote{This is due to Tarski,
see~\citeauthor{Jech-AC}\footnotemark{}, p.~107.}\footcitetext{Jech-AC}
The axiom of choice is a principle that we may add to our type theory
(it holds in the standard model), but there are many models where it doesn't hold.
\begin{principle}[The Axiom of Choice]\label{pri:ac}
For every set $X$ and every family of \emph{non-empty} sets
$P : X \to \Set_{\ne\emptyset}$,
there exists an dependent function of type $\prod_{x:X}P(x)$.
In other terms, for any set $X$ and any family of sets $P:X\to\Set$,
we have
\begin{equation}\label{eq:ac-impl}
\prod_{x:X}\Trunc{P(x)} \to \Trunc[\bigg]{\prod_{x:X}P(x)}.\qedhere
\end{equation}
\end{principle}
\begin{remark}
We have an equivalence between the Pi-type $\prod_{x:X}P(x)$ and the
type of sections of the projection map $\prj_1 : \sum_{x:X}P(x) \to X$,
under which families of non-empty sets correspond to surjections between sets
(using that $X$ is a set).
Thus, the axiom of choice equivalently says that any surjection
between sets admits a section.
Because of this equivalence, we'll sometimes also call elements of the
Pi-type \emph{sections}.
\end{remark}
The following is usually called Diaconescu's theorem\footcite{Diaconescu} or the Goodman--Myhill theorem\footcite{Goodman-Myhill}, but it was first observed in a problem in Bishop's book on constructive analysis~\footcite{Bishop}.
\begin{theorem}
The axiom of choice implies the law of the excluded middle, \cref{pri:lem}.
\end{theorem}
\begin{proof}
Let $P$ be a proposition, and consider the quotient map $q : \bn 2 \to \bn 2/\sim$,
where $\sim$ is the equivalence relation on $\bn 2$ satisfying $(0 \sim 1) = P$.
Like any quotient map, $q$ is surjective, so by the axiom of choice,
and because our goal is a proposition,
it has a section $s : \bn 2/\sim \to \bn 2$.
That is, we also have $q\circ s = \id$.
Using decidable equality in $\bn 2$, check whether $s([0])$ and $s([1])$ are equal
or not.
If they are, then we get the chain of identifications
$[0] = q(s([0])) = q(s([1])) = [1]$, so $P$ holds.
If they aren't, then assuming $P$ leads to a contradiction, meaning $\lnot P$ holds.
\end{proof}
We'll now define some restricted variants of the axiom of choice,
that however are not always true,
and our goal is to see how they relate to each other and to other principles.
\begin{definition}
Let $\AC$ denote the full axiom of choice, as in~\cref{pri:ac}.
If we fix the set $X$, and consider \eqref{eq:ac-impl} for arbitrary families $P:X\to\Set$, we call this the \emph{$X$-local axiom of choice}, denoted $\lAC{X}$.
If we restrict $P$ to take values in $n$-element sets, for some $n:\NN$,
we denote the resulting principle $\AC(n)$.
(That is, here we consider families $P : X \to \BSG_n$.)
If we both fix $X$ and restrict to families of $n$-element sets,
we denote the resulting principle $\lAC{X}(n)$.
\end{definition}
\begin{xca}
Show that $\lAC{X}$ is always true whenever $X$ is a finite set.
\end{xca}
\begin{lemma}\label{lem:ac-impl-triv-coh-sets}
If $\lAC{X}$ holds for a set $X$,\marginnote{%
In fancier language, this says that the axiom of choice
implies that all cohomology sets $\constant{H}^1(X,G)$ are trivial.}
then $\Trunc{X \to \BG}_0$ is contractible for any group $G$.
\end{lemma}
\begin{proof}
Suppose we have a map $f : X \to \BG$.
We need to show that $f$ is merely equal to the constant map.
Consider the corresponding family of sets
consisting of the underlying sets of the $G$-torsors represented by
$f(x) : BG$, for $x:X$.
That is, define $P : X \to \Set$ by setting $P(x) \defeq (\shape_G = f(x))$.
Since $\BG$ is connected, this is a family of non-empty sets,
so by the axiom of choice for families over $X$,
there exists a section.
Since we're proving a proposition, let $s : \prod_{x:X}(\shape_G = f(x))$
be a section.
Then $s$ identifies $f$ with the constant map, as desired.
\end{proof}
We might wonder what happens if we consider general \inftygps $G$
in~\cref{lem:ac-impl-triv-coh-sets}.
Then the underlying type of a $G$-torsor is no longer a set, but can be any type.
Correspondingly, we need an even stronger version of the axiom of choice,
where the family $P$ is allowed to be arbitrary.
Let $\AC_\infty$ denote this untruncated axiom of choice,
and let $\lAC{X}_\infty$ denote let local version, fixing a set $X$.
This is connected to another principle, which is much more constructive,
yet still not true in all models.
\begin{principle}[Sets Cover]\label{pri:sc}
For any type $A$, there exists a set $X$ together with a surjection $X \to A$.
\end{principle}
We abbreviate this as $\constant{SC}$.
\begin{xca}
Prove that the untruncated axiom of choice, $\AC_\infty$,
is equivalent to the conjunction of the standard axiom of choice, $\AC$,
and the principle that sets cover, $\constant{SC}$.
\end{xca}
\begin{xca}
Prove that we cannot relax the requirement that $X$ is a set
in the axiom of choice.
Specifically, prove that $\lAC{\Sc}(2)$ is false
\end{xca}
We now come to the analogue of~\cref{lem:ac-impl-triv-coh-sets}
for arbitrary \inftygps.
\begin{xca}
Prove that if the untruncated $X$-local axiom of choice, $\lAC{X}_\infty$,
holds for a set $X$,
then $\Trunc{X \to \BG}_0$ is contractible for all \inftygps $G$.
\end{xca}
We now discuss two partial converses to~\cref{lem:ac-impl-triv-coh-sets},
both due to \citeauthor{Blass-Finite-Choice}\footcite{Blass-Finite-Choice}.
\begin{theorem}[Blass]\label{thm:Blass-1}
Let $X$ be a set such that $\Trunc{X \to \BG}_0$ is contractible
for all groups $G$.
Then every family of non-empty sets over $X$, $P : X \to \Set$,
that factors through a connected component of $\Set$,
merely admits a section.
\end{theorem}
\begin{proof}
We suppose $P : X \to \Set$ is such that all the sets $P(x)$
have the same size, \ie the function $P$ factors through
$\BAut(S)$ for some non-empty set $S$.
This in turn means that we have a function $h : X \to \BG$,
where $G \defeq \Aut(S)$, with $P = \prj_1 \circ h$,
where $\prj_1 : \BAut(S) = \sum_{A : \Set}\Trunc{S \simeq A} \to \Set$
is the projection.
By assumption, $h$ is merely equal to the constant family.
But since we are proving a proposition, we may assume that $h$
\emph{is} constant, so $P$ is the constant family at $S$.
And this has a section since $S$ is non-empty.
\end{proof}
Obviously, the same argument works if we consider all \inftygps $G$
and families of types that are all equivalent.
For the second partial converse, we look at decidable sets.
\begin{theorem}[Blass]\label{thm:Blass-2}
Let $X$ be a decidable set such that $\Trunc{X \to \BG}_0$ is contractible
for all groups $G$.
Then every family of non-empty decidable sets over $X$
merely admits a section.\footnote{%
We might call this conclusion $\lAC{X}^{\mathrm{dec}}$.}
\end{theorem}
\begin{proof}
Equivalently, consider a surjection $p : Y \to X$,
where $X$ and $Y$ are decidable sets,
and let $C$ be the higher inductive type with constructors
$c : C$, $f : X \to C$, and $k : \prod_{y:Y}(c = f(p(y))$.\footnote{%
This kind of higher inductive type is also known as a pushout,
and its constructors fit together to give a commutative square:
\[
\begin{tikzcd}[ampersand replacement=\&]
Y \ar[d]\ar[r,"p"] \& X \ar[d,"f"] \\
\bn 1 \ar[r,"c"'] \& C
\end{tikzcd}
\]}
Using the same kind of argument as in~\cref{lem:wedgeofgpoidisgpoid}
and~\cref{thm:free-group-elements}, we can show,
using decidability of equality in $X$ and $Y$,
that the identity type $c =_C f(x)$ is equivalent to a type of reduced words
over $Y \coprod Y$.
In particular, $C$ is a groupoid, and it's easy to check that it's connected.
Hence we can form the group $G \defeq \mkgroup(C,c)$.
By assumption, the map $f$ is merely equal to the constant map,
so since we're proving a proposition,
we may assume we have a family of elements $h(x) : c = f(x)$, for $x:X$.
Taking for each $x$ the last $y$ in the corresponding reduced word,
we get a family of elements $s(x) : Y$
such that $p(s(x)) = x$,
but this is precisely the section we wanted.
\end{proof}
It seems to be an open problem, whether we can do without the decidability assumption,
\ie whether the converse of~\cref{lem:ac-impl-triv-coh-sets} holds generally.
Now we turn as promised to the connections between the various local choice principles
$\lAC{X}(n)$.
The simplest example is the following.
\begin{theorem}\label{thm:lAC-2-3-4}
Let $X$ be any set. Then $\lAC{X}(4)$ follows from $\lAC{X}(2)$ and $\lAC{X}(3)$.
\end{theorem}
\begin{proof}
Let $P : X \to \BSG_4$ be a family of $4$-element sets over $X$.
Consider the map $\Bf : \BSG_4 \to \BSG_3$ that maps a $4$-element set
to the $3$-element set of its $2+2$ partitions.
Choose a section of $\Bf \circ P$ by $\lAC{X}(3)$.
Now use $\lAC{X}(2)$ twice to choose for each chosen partition
first one of the $2$-element parts, and secondly one of the $2$
elements in each chosen part.
\end{proof}
We now look a bit more closely at what happened in this proof,
so as to better understand the general theorem.
The key idea is the concept of ``reduction of the structure group''.
[TODO, Elaborate: For a family of $n$-element sets over a base type $X$, $P : X
\to \BSG_n$, there is a section if and only if there is a
`` to a subgroup of $\SG_n$,
whose action on the standard $n$-element set, $\bn n$, has a fixed point.]
Now we return to the local case, and we give the general
sufficient condition that ensures that $\lAC{X}(n)$ follows from $\lAC{X}(z)$ for each $z:Z$, where $Z$ is a finite subset of $\NN$.
\begin{definition}
The condition $L(Z,n)$ is that for every finite subgroup $G$ of $\SG_n$
that acts on $\bn n$ without fixed points,
there exists finitely many proper, finite subgroups $K_1,\cdots,K_r$ of
$G$ such that the sum of the indices,
\[
|G \idxcolon H_1| + \cdots + |G \idxcolon H_r|,
\]
lies in $Z$.
\end{definition}
We now turn to the global case, where we can change the base set.
Here the basic case is Tarski's result alluded to above,
which shows that we don't need choice for $3$-element sets,
in contrast to the local case, \cref{thm:lAC-2-3-4}.
\begin{theorem}
$\AC(2)$ implies $\AC(4)$.
\end{theorem}
\begin{proof}
Let $P: X \to \BSG_4$ be a family of $4$-element sets indexed by a set $X$.
Consider the new set $Y$ consisting of all $2$-element subsets
of $P(x)$, as $x$ runs over $X$,
\[
Y \defeq \sum_{x:X}[P(x)]^2.
\]
The set $Y$ carries a canonical family of $2$-element sets,
so we may choose an element of each.
In other words, we have chosen an element of each of the $6$
different $2$-element subsets of each of the $4$-element sets
$P(x)$.
For every $a : P(x)$, let $q_x(a)$ be the number of $2$-element
subsets $\set{a,b}$ of $P(x)$ with $b\ne a$ for which $a$ is the
chosen element.
Define the sets $B(x) \defeq \setof{a:P(x)}{\text{$q_x(a)$ is a
minimum of $q_x$}}$, and remember that they are subsets of $P(x)$.
This determines a decomposition of $X$ into three parts $X = X_1 +
X_2 + X_3$, where
\[
X_i \defeq \sum_{x:X}(\text{$B(x)$ has cardinality $i$}),
\quad i = 1,2,3.
\]
Note that $B(x)$ can't be all of $P(x)$,
since that would mean that $q_x$ is constant,
and that is impossible, since the sum of $q_x$ over the $4$-element $P(x)$ is $6$.
Over $X_1$, we get a section of $P$ by picking the unique element
in $B(x)$.
Over $X_3$, we get a section of $P$ by picking the unique element
\emph{not} in $B(x)$.
Over $X_2$, we get a section of $P$ by picking the already chosen
element of the $2$-element set $B(x)$.
\end{proof}
The following appears as Theorem~6 in Blass\footcite{Blass-Finite-Choice}.
\begin{theorem}
Assume $\Trunc{X \to \BCG_n}_0$ is contractible for all sets $X$ and
positive integers $n$. Then $\AC(n)$ holds for all $n$.
\end{theorem}
\begin{proof}
We use well-founded induction on $n$, the case $n\jdeq 1$ being trivial.
Let $P : X \to \BSG_n$ be a family of $n$-element sets,
and let $Y \defeq \sum_{x:X}P(x)$ be the domain set of this \covering.
Consider the family $Q : Y \to \BSG_{n-1}$ defined by
\[
Q((x,y)) \defeq \setof{y' : P(x)}{y \ne y'} = P(x) \setminus \set{y},
\]
where we use the fact that $P(x)$ is an $n$-element set
and thus has decidable equality,
so we can form the $(n-1)$-element complement $P(x) \setminus
\set{y}$.
By induction hypothesis, we get a section of $Q$, which we can
express as a family of functions
\[
f : \prod_{x:X}\bigl(P(x) \to P(x)\bigr)
\]
where $f_x(y) \ne y$ for all $x,y$.
Since $P(x)$ is an $n$-element set, we can decide whether $f_x$
is a permutation or not, and if so, whether it is a cyclic
permutation.
We have thus obtained a partition $X = X_1 + X_2 + X_3$,
where
\begin{align*}
X_1 &\defeq \setof{x:X}{\text{$f_x$ is not a permutation}}, \\
X_2 &\defeq \setof{x:X}{\text{$f_x$ is a non-cyclic permutation}}, \\
X_3 &\defeq \setof{x:X}{\text{$f_x$ is a cyclic permutation}}.
\end{align*}
We get a section of $P$ over $X_1$ by induction hypothesis
by considering the family of the images of $f_x$.
We get a section of $P$ over $X_2$ by first choosing a cycle of $f_x$
(there are fewer then $n$ cycles because there are no $1$-cycles),
and then choosing an element of the chosen cycle.
We get a section of $P$ over $X_3$ by the assumption applied
to the map $X_3 \to \BCG_n$ induced by equipping each $P(x)$ with
the cyclic order determined by the cyclic permutation $f_x$.
\end{proof}
[TODO: State the general positive result due to
Mostowski\footcite{Mostowski-Finite-Choice}, maybe as an exercise
and give references to the negative results, due to Gauntt (unpublished).]
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: