axiom of choice in nLab

The axiom of choice

The axiom of choice

Statement

The axiom of choice is the following statement:

• Every surjection in the category Set of sets splits.

This means: for every surjection f:A→Bf\colon A \to B of sets, there is a function σ:B→A\sigma\colon B \to A (a section), such that

(B→σA→fB)=(B→Id BB). (B \stackrel{\sigma}{\to} A \stackrel{f}{\to} B) = (B \stackrel{Id_B}{\to} B) \,.

Note that a surjection A→BA \to B of sets can be regarded as a BB-indexed family of inhabited sets, while the existence of a section is equivalent to a choice of one element in each set of this family. This reproduces the more classical form of the axiom of choice.

When the full axiom of choice fails, it may still be valid for some restricted class of objects AA and/or BB. An object BB such that any epimorphism A→BA \to B splits is called projective; this means that one can make choices ‘indexed by’ BB. Dually, an object AA such that one can make choices ‘with values in’ AA is called a choice object (this is not quite equivalent to every epimorphism A→BA \to B splitting).

In other categories

More generally, we may consider analogous statements in categories CC other than SetSet.

External form

We say that CC satisfies the external axiom of choice if every epimorphism in CC splits.

In this form, the axiom of choice may look less mysterious than in its original formulation. For instance, it is clear that it fails in contexts such as C=C = Top and C=C = Diff, due to the existence of nontrivial topological and smooth fiber bundles.

If CC is not balanced, such as a regular or coherent category which is not a pretopos, it may be more appropriate to replace in this statement “epimorphism” by regular epimorphism (or extremal epimorphism, effective epimorphism, etc.) In SetSet (and in any topos), all of these notions of epimorphism are the same.

More generally still, if CC is a site, then the axiom of choice for CC may be taken to say that any cover U→XU\to X admits a section. Obviously this refers only to singleton covers, but if CC is superextensive then any covering family (p i:U i→X) i(p_i\colon U_i \to X)_i can be replaced by a singleton cover ∐ uU i→X\coprod_u U_i \to X.

Internal form

However, when working in a category that has an internal logic, we may want to “internalize” the axiom of choice by asserting, not that every epimorphism has a section, but that the statement “every epimorphism has a section” is true in the internal logic (or more precisely the stack semantics). An equivalent statement is that every object is internally projective. We call this the internal axiom of choice.

This is generally a weaker statement: a topos satisfies the external AC if and only if it satisfies the internal AC and also (the external form of) supports split. Often, however, this is the more relevant notion to consider.

The following characterization can be found in Freyd-Scedrov (1990, p.181)

In particular, satisfaction of IAC entails Booleanness.

Classical examples of Boolean étendues are provided by toposes of group actions hence these all satisfy IAC but satisfy AC only in case the group is trivial (cf. Johnstone 1977, p.144 or Freyd-Scedrov 1990, p.84, 179)).

If a topos CC satisfies IAC, then so do all of its slice categories, although this may not be obvious. See this answer.

In toposes

Equivalents

The following statements are all equivalent to the axiom of choice in SetSet (although sometimes the proof in one direction requires excluded middle). This is a very short list; much longer lists can be found elsewhere, such as at Wikipedia. Some of the statements on this list, though, may be of interest to nLabbers but are not commonly mentioned as equivalents of choice.

• That any cartesian product of any family of inhabited sets is inhabited.

• That given a surjection ff and an element bb in the codomain of ff, the preimage f *(b)f^*(b) of ff at bb has a (local) choice operator, a function ϵ:[f *(b)]→f *(b)\epsilon:[f^*(b)] \to f^*(b) from the support of f *(b)f^*(b) to f *(b)f^*(b) itself.

• The well-ordering theorem (that any set can be well-ordered),

• Zorn's lemma,

• That (L=L = monomorphisms, R=R = epimorphisms) is a weak factorization system on Set.

• That Set is equivalent to its own free exact completion.

• That there exists a group structure on every inhabited set (see Hartogs number, or this MO answer).

• That every essentially surjective functor between small strict categories is split essentially surjective.

• That every fully faithful and essentially surjective functor between small strict categories is a strong equivalence of categories.

• That the nonabelian cohomology H 1(X;G)H^1(X;G) is trivial for every set XX and every group GG (see this post).

• If XX and YY are infinite sets and the two free groups F(X)F(X) and F(Y)F(Y) have equal cardinality, then XX and YY also have equal cardinality (see Kleppmann14).

• That every vector space is free.

Variants

There are a number of weaker axioms which are implied by the full axiom of choice. Some of these are valid or accepted more generally than the full AC, and/or suffice for some of the usual applications of choice. In particular, the full axiom of choice is generally rejected in constructive mathematics, whereas some of these weaker forms of choice may be accepted, such as (in order of increasing strength) countable choice, dependent choice, and COSHEP.

• Many applications of choice in logic, topology, and algebra require only the ultrafilter principle (UF), or equivalently the Boolean prime ideal theorem.

• From the perspective of constructive mathematics, the principle of excluded middle (EM) may be seen as a weak form of the axiom of choice; EM is equivalent to the statement that every Kuratowski-finite set is projective. See at Diaconescu-Goodman-Myhill theorem.

• A very weak form of choice (which follows from EM) is the statement that supports split in SetSet.

• The axioms of countable choice (CC) and dependent choice (DC) suffice for many of the usual applications of choice in the analysis of separable spaces. CC states that the set ℕ\mathbb{N} of natural numbers is projective. DC strenghtens CC by allowing the set of possible choices for n+1n+1 to depend on the choice made for nn.

• The axiom COSHEP, also called the “presentation axiom,” says that any set admits a surjection from a projective one (whereas full AC says that all sets are projective). This implies CC and DC, and is moreover sufficient for the existence of projective resolutions and cofibrant replacements, as well as the usual theorems in algebra that (for example) Mod has enough projectives. For example, see the canonical model structure on Cat.

• The axiom of small violations of choice (SVC) asserts there is a set SS such that every set is a subquotient of C×SC\times S for some choice set CC. Intuitively, this says that the failure of AC is parametrized by a single set. It can be regarded as a “dual” of COSHEP, since it deals with choice sets rather than projective ones, it implies the existence of (at least some) injective resolutions, and together with COSHEP and EM it implies full AC.

• The axiom of multiple choice is a different way of saying that choice is violated in only a small way, which is more “local” than SVC. It apparently follows from SVC, at least in ZF.

• The small cardinality selection axiom is another similar axiom. It asserts that there is a class function selecting for every set an isomorphic set (its “cardinality”) such that among each isomorphism class of sets, the collection of all “cardinalities” forms only a set.

• A still weaker axiom along the lines of “AC fails in only a small way,” which is implied by AMC, is WISC, i.e. that for any set XX, the full subcategory of Set/XSet/X consisting of the surjections has a weakly initial set (under COSHEP it has a single weakly initial object, namely a projective cover of XX). Two similar assertions are that the free exact completion Set ex/lexSet_{ex/lex} of SetSet is a topos (i.e. that SetSet has a generic proof), and that Set ex/lexSet_{ex/lex} is well-powered; both of these imply WISC.

• In constructive mathematics, there is also decidable choice, where every set with decidable equality is projective.

The axiom of choice can also be strengthened in a few ways.

• While the ordinary axiom of choice says that any surjection of sets is split, the axiom of global choice says that this is also true for any surjection of proper classes. (Making this precise requires a bit of work.) It is equivalent to the existence of a well-ordering of the class of all sets.

• One can also postulate a choice operator, which gives a specified way to choose an element from any nonempty set. This implies global choice, and conversely a choice operator can be defined from any well-ordering of the class of all sets.

Finally, one can instead adopt the negation of the axiom of choice, or a strengthened version of this negation:

• The assumption that every subset of the real line has the Baire property (BP) is consistent with DC but not AC; the same holds for the assumption that every subset of the real line is measurable (LM) if at least one Grothendieck universe exists. These assumptions leads to a very nice setting for analysis called dream mathematics.

• The axiom of determinacy is a natural statement in game theory that is consistent with DC; in fact, it implies DC in certain models, such as in the constructible (in the sense of Goedel) closure of the set of reals. However, determinacy contradicts full AC (for example, it implies LM and BP, as in the previous entry).

• Any of the varieties of constructive mathematics that contradict excluded middle necessarily contradict choice, but they are usually (if not always) consistent with DC (and even COSHEP).

• The existence of a Reinhardt cardinal contradicts AC.

In higher category theory

To formulate a version of the axiom of choice in a higher category, one has to make an appropriate choice of the meaning of “epimorphism”. In most cases, it is best to choose effective epimorphism in an (infinity,1)-category or a related notion such as eso morphisms.

Less obviously, we usually want to also impose truncation requirements on at least some of the objects involved in the axiom of choice. It seems usually necessary to require the codomain to be 0-truncated (axioms of choice without this requirement tend to be inconsistent); as for the domain we can choose to or not.

• An (∞,1)(\infty,1)-category satisfies the axiom of nn-choice, or AC nAC_n, if every nn-truncated morphism? with 0-truncated codomain has a section. We write AC ∞AC_\infty for the axiom of infinity-choice: the statement that every morphism with 0-truncated codomain has a section.

These are stronger axioms as nn increases. The “difference” between AC 0AC_0 and AC ∞AC_\infty is roughly the axiom that sets cover.

For (n,k)(n,k)-categories with k>1k\gt 1 it is unclear whether it is sensible to allow the domain to be non-groupoidal.

• In 2-category theory, the axiom of 2-choice has been proposed to mean that every eso morphism with groupoidal domain and 0-truncated codomain has a section.

There are also “internal” versions of these axioms.

• In homotopy type theory (the internal logic of an (∞,1)(\infty,1)-topos), the internal version of AC nAC_n is “every surjection onto a set with nn-type fibers has a section”, or equivalently

  ∏ (X:Set)∏ (Y:X→nType)(∏ (x:X)‖Y(x)‖→‖∏ (x:X)Y(x)‖) \prod_{(X:Set)} \prod_{(Y:X\to n Type)} \Big( \prod_{(x:X)} \Vert Y(x)\Vert \to \Big\Vert \prod_{(x:X)} Y(x) \Big\Vert \Big)

• More generally, we can replace the (−1)(-1)-truncation by the kk-truncation to obtain a family of axioms AC k,nAC_{k,n}.

• We can also replace the (−1)(-1)-truncation by the assertion of kk-connectedness, obtaining the axiom of kk-connected choice.

In type theory

In dependent type theory, there are two interpretations of predicate logic in the type theory; propositions as some types and propositions as types, resulting in two notions of the axiom of choice:

• propositional axiom of choice

• type theoretic axiom of choice

The former corresponds to the internal axiom of choice in categorical semantics and set theory, while the latter is provable in any locally cartesian closed category or the set theory which interprets such categories.

In spatial type theory

In spatial type theory, which is dependent type theory with the sharp modality and the flat modality, there exists a version of the axiom of choice called the sharp axiom of choice, which is given by the following inference rule:

Γ⊢AtypeΓ,x:A⊢B(x)typeΓ⊢ac A,B ♯:(∏ x:A♯[B(x)])→♯∀x:A.♯B(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ac}^{\sharp}_{A, B}:\left(\prod_{x:A} \sharp [B(x)]\right) \to \sharp\forall x:A.\sharp B(x)}

where ♯A\sharp A is the sharp modality of type AA, [A][A] is the propositional truncation of AA, and the universal quantifier ∀x:A.B(x)\forall x:A.B(x) is the propositional truncation of the dependent product type ∏ x:AB(x)\prod_{x:A} B(x).

Consequences

• The axiom of choice implies the principle of excluded middle (due to Diaconesu 1975) see McLarty, theorem 17.9, and see at excluded middle – Relation to axiom of choice

See also the choice consequences data base

• propositional axiom of choice

• well-ordering

• anafunctor

• foundations

• Boolean topos

• finite choice

References

General

• Eric Schechter's analysis book surveys several variants of AC and its negation with a view to applications of analysis, including this nice picture:

(Here, UF, DC, CC, BP, and LM are as defined above.)

Discussion in toposes is in

• Colin McLarty, section 17.6 of Elementary Categories, Elementary Toposes

• The Consequences of the Axiom of Choice Project provides an interactive data base that can be used to search for implications between various (weakened) forms of the Axiom of Choice. Choiceless grapher (cf. github.com/ioannad/jeffrey) builds on this data and provides a graphical presentation.

• Gonçalo Gutierres da Conceição, The Axiom of Countable Choice in Topology, pdf

  Despite the title, this covers more than countable choice, but the focus is on sequential aspects (metric spaces, first- and second-countable spaces, etc).

A classical reference for AC in toposes is section 5.2 (pp.140ff) in

• Peter Johnstone, Topos Theory , Academic Press New York 1977. (Reprinted by Dover Mineola 2014)

Relation to cohomology is discussed in

• Andreas Blass, Cohomology detects failures of the axiom of choice, Trans. Amer. Math. Soc. 279 (1983), 257-269 (web)

• Mike Shulman, Cohomology on the homotopy type theory blog here

and to free groups in

• Philipp Kleppmann, Generating sets of free groups and the axiom of choice, Mathematical Logic Quarterly, 2014, doi

An alternative form of AC in toposes using injectivity is explored in

• Toby Kenney, Injective Power Objects and the Axiom of Choice , JPAA 215 (2011) pp.131–144.

The result on IAC in toposes stems from

• P. J. Freyd, A. Scedrov, Categories, Allegories , North-Holland Amsterdam 1990.

In homotopy type theory

Discussion in homotopy type theory:

• Univalent Foundations Project, section 3.8 of Homotopy Type Theory – Univalent Foundations of Mathematics

• Egbert Rijke, section 17.4 of Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)

In spatial type theory

For the sharp axiom of choice in spatial type theory, see:

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)