Dualizing real vector-space sequences and the choice boundary

Assume AC. For a subspace $A\subset B$, apply [F1] to the empty independent set in $A$ to obtain a basis $S$, and then to $S\subset B$ to obtain a basis $T$ of $B$ containing $S$. If $a\in A^{\ast }$, assign value $a(s)$ at $s\in S$ and value zero at $t\in T\setminus S$. A vector of $B$ has a unique finite expression in $T$, so the corresponding finite sum defines a real-linear functional $b$ on $B$. For a vector in $A$, its expression in $S$ is also its expression in $T$, and hence $b{\mathrm{\mid }}_A=a$. These two basis constructions are the exact AC use. If $A=0$, take the zero extension directly; if $A=B$, take $b=a$.

For an arbitrary short exact sequence as stated, transport a functional on $A$ to the subspace $i(A)$ using the inverse of the injective map $i$, and apply step 1.1. Thus $i^{\ast }$ is surjective. Since $q$ is surjective, $f\circ q=0$ implies $f=0$, so $q^{\ast }$ is injective. The composite $i^{\ast }{q}^{\ast }$ is zero since $qi=0$. Conversely, if $b\circ i=0$, define $\bar{b}(d)=b(x)$ for any $x$ with $q(x)=d$. Such an $x$ exists; two choices differ by an element of $\ker q=i(A)$ on which $b$ vanishes. This uniquely specifies $\bar{b}$ without selecting lifts. It is linear by applying $b$ to sums and scalar multiples of any lifts, and $q^{\ast }\bar{b}=b$. Hence $\ker i^{\ast }=\mathrm{im}{q}^{\ast }$. Only the surjectivity argument used AC. This also covers $B=0$ and the endpoint cases $A=0$ or $D=0$.

In contrast to the AC conclusion of step 2.1, for the second branch assume only ZF + DC and the stated Baire-property hypothesis. On $P$ use the metric $d(x,y)={\sum }_{n\ge 0}{2}^{-n-1}\min (1,\mathrm{\mid }{x}_n-y_n\mathrm{\mid })\mathrm{.}$ The triangle inequality follows termwise from that of $\min (1,\mathrm{\mid }s-t\mathrm{\mid })$; positivity and symmetry are immediate. This metric induces the product topology. Indeed a sufficiently small metric ball forces any prescribed finite set of coordinate inequalities, by the individual positive weights. Conversely a small restriction on finitely many initial coordinates makes the corresponding partial sum small, while the geometric tail is arbitrarily small. A metric Cauchy sequence is Cauchy in each real coordinate, so let $x_n$ be its unique coordinate limit. These unique limits define $x\in P$. For any $ϵ>0$, bound the geometric tail by $ϵ\mathrm{/}2$ and use convergence in the finitely many initial coordinates for the remaining $ϵ\mathrm{/}2$. This proves convergence to $x$ in $d$, so $P$ is complete. It is nonempty, containing the zero sequence. By [F2], no nonempty open subset of $P$ is meager: replace the nowhere dense sets by their closed closures and intersect their open dense complements with that open subset.

We will use the fact that a countable union of meager sets is meager under DC, and spell out its selection cost. If $M_j$ is meager, let ${\mathcal{W}}_j$ be the nonempty set of sequences of nowhere dense subsets covering $M_j$. The set of finite tuples $(w_0,\dots ,w_{k-1})$ with $w_j\in {\mathcal{W}}_j$ contains the empty tuple, and extension by one more coordinate is an entire relation: for that one index a witness exists. DC starting at the empty tuple produces a chain of such extensions. Its union gives one $w_j$ for every $j$. A fixed enumeration of $\mathbb{N}\times \mathbb{N}$ now gives a single sequence of nowhere dense sets covering ${\bigcup }_j{M}_j$. This is the only countable family of meagerness witnesses selected below.

Let $L:P\to \mathbb{R}$ be any algebraic linear functional. The sets $A_m=\{x:\mathrm{\mid }L(x)\mathrm{\mid }\le m\}$ for integers $m\ge 1$ cover $P$. By steps 3.1 and 4.1, some $A_m$ is nonmeager. By the Baire-property hypothesis there are an open set $O$ and a meager set $N$ with $A_m\mathrm{△}O\subseteq N$. The set $O$ is nonempty, since otherwise $A_m$ is meager. Take $a\in O$ and a symmetric open neighborhood $V$ of zero with $a+V+V\subseteq O$; such a $V$ is obtained by shrinking the finitely many coordinate intervals of a basic neighborhood at $a$. For $t\in V$, the nonempty open set $a+V$ lies in both $O$ and $O-t$. Translations preserve nowhere density and meagerness since they are homeomorphisms. Hence $N\cup (N-t)$ is meager and cannot cover $a+V$. There is therefore $b\in (a+V)\setminus (N\cup (N-t))$. Then $b,b+t\in A_m$, giving $\mathrm{\mid }L(t)\mathrm{\mid }=\mathrm{\mid }L(b+t)-L(b)\mathrm{\mid }\le 2m$. This proves that $L$ is bounded on $V$. For each $ϵ>0$, choose an integer $k>2m\mathrm{/}ϵ$; on the open neighborhood $k^{-1}V$ its absolute value is less than $ϵ$. Thus $L$ is continuous. No $b$ is chosen simultaneously for all $t$; the argument proves the bound separately for each $t$.

Continuity supplies a basic product neighborhood $W$ of zero on which $\mathrm{\mid }L\mathrm{\mid }<1$. Let $F\subset \mathbb{N}$ be the finite set of coordinates restricted by $W$. If $y$ vanishes on $F$, then $ry\in W$ for every real $r$, so $\mathrm{\mid }rL(y)\mathrm{\mid }<1$ for every $r$, which forces $L(y)=0$. In particular, if $e_n$ is the sequence with its only nonzero coordinate equal to one at $n$, then $L(e_n)=0$ for all $n\mathrm{\notin }F$. But the well-defined finite-sum functional $\mathrm{\ell }:E\to \mathbb{R}$ satisfies $\mathrm{\ell }(e_n)=1$ for every $n$. The least integer outside $F$ supplies a contradiction to $L{\mathrm{\mid }}_E=\mathrm{\ell }$. Thus restriction $P^{\ast }\to E^{\ast }$ is not surjective. The inclusion and quotient give an exact sequence $0\to E\to P\to P\mathrm{/}E\to 0$ in ZF, so this is the claimed failure of exactness after dualization.

In this witness $E$ is nonzero because $e_0\in E$ is nonzero, and $P\mathrm{/}E$ is nonzero because the constant-one sequence has infinite support. No quotient representatives are chosen to define the sequence. The zero functional always extends, but the explicitly given $\mathrm{\ell }$ does not in this branch. The functional $\mathrm{\ell }$ is well-defined on vectors with any finite support, including empty support, and no sign or order of summation is ambiguous because each sum is finite. The supplied-simplex construction in [F3] instead already has a containing basis, so its zero extension does not call on step 1.1 or on either additional axiom of this second branch.