Practice: The axiom of choice and its equivalents

The axiom of choice and its equivalents

Warm-upHuman

Which of these choice tasks genuinely needs (some form of) the axiom of choice?

Choose one

Choose an element from each non-empty subset of

\N

Choose one element from each of five non-empty setsChoose one sock from each of countably many pairs of indistinguishable socksChoose a point from each non-empty closed interval

[a, b]

with

a \le b

The axiom of choice and its equivalents

CoreHuman

In the proof that every vector space has a basis, why is the union of a chain $C$ of linearly independent sets again linearly independent?

Choose one

A dependence involves finitely many vectors, which all lie in a single member of the chainBecause a union of independent sets is always independentBecause the chain is countableBecause the union spans the space

The axiom of choice and its equivalents

CoreHuman

In Krull's theorem, why is the union $U$ of a non-empty chain of proper ideals again proper?

Choose one

Because

1

lies in no member of the chain, so

1 \notin U

Because a union of proper subsets is always properBecause the chain has a largest elementBecause

R

is commutative

The axiom of choice and its equivalents

CoreHuman

How many (unordered) bases does the vector space $(\Z/2)^3$ have?

The axiom of choice and its equivalents

Warm-upHuman

How many maximal ideals does the ring $\Z/360$ have?

The axiom of choice and its equivalents

StretchHuman

Which of these are provable in ZF, without any form of choice? Select all.

Choose all that apply

Every surjection

p : \N \to A

has a sectionIf every set can be well-ordered, then AC holdsEvery surjection

p : \R \to A

has a sectionA countable union of countable sets is countableThe Schröder–Bernstein theorem

The axiom of choice and its equivalents

CoreFormal

Which Lean proposition expresses the axiom of choice (for families indexed by a type ι)?

Choose one

∀ (ι : Type) (X : ι → Type), (∀ i, Nonempty (X i)) → Nonempty (∀ i, X i)∀ (ι : Type) (X : ι → Type), Nonempty (∀ i, X i) → ∀ i, Nonempty (X i)∀ (ι : Type) (X : ι → Type), (∃ i, Nonempty (X i)) → Nonempty (∀ i, X i)∀ (ι : Type) (X : ι → Type), Nonempty (Σ i, X i)

The axiom of choice and its equivalents

StretchHuman

In the proof of Diaconescu's theorem, with $U = \{x \in \{0, 1\} \mid x = 0 \lor p\}$ and $V = \{x \in \{0, 1\} \mid x = 1 \lor p\}$ , where exactly is extensionality used?

Choose one

To conclude

U = V

(and hence

f(U) = f(V)

) from the assumption

p

To show that

U

and

V

are non-emptyTo decide whether

f(U) = 0

or

f(U) = 1

It is not used; the proof works without it

The axiom of choice and its equivalents

StretchComputational

Vectors in $(\Z/2)^n$ are stored as integers whose binary digits are the coordinates; vector addition is XOR (^). Write span(vectors) returning the set of all sums of subsets of vectors (including 0), and extend_to_basis(start, n) that starts from the linearly independent list start and goes through 1, 2, ..., 2**n - 1, appending every vector not already in the span. It should return the resulting list — a basis containing start.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.