TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Assuming choice, $J_{V} : V \to V^{* *}$ is surjective if and only if $V$ is finite-dimensional

Statement

Assume the axiom of choice. The canonical map $J_{V} : V \to V^{* *}$ is surjective if and only if $V$ is finite-dimensional.

Facts & Assumptions

Given: The axiom of choice and an $F$ -vector space $V$ .

[L1]

The canonical map is linear and injective (Assuming choice, the canonical map $J_{V} : V \to V^{* *}$ is linear and injective).

[L2]

For a finite basis $(b_{i})$ , its dual family $(b_{i}^{*})$ is a basis of $V^{*}$ (The dual family of a finite basis is a basis of the dual space, with the same dimension).

[L3]

For an infinite Hamel basis $B$ , its coordinate functionals span a proper subspace of $V^{*}$ (For an infinite Hamel basis, its dual family is linearly independent but does not span the algebraic dual).

[L4]

Assuming choice, a vector outside a subspace is separated from it by a linear functional (Assuming choice, if $v \notin U \leq V$ , some $f \in V^{*}$ vanishes on $U$ and satisfies $f (v) = 1$ ).

[L5]

Assuming choice, every vector space has a basis (Every vector space has a basis); for an infinite-dimensional $V$ such a basis is infinite.

Proof

technique · direct, proving both implications

1.1

Suppose $V$ has finite basis $(b_{1}, \dots, b_{n})$ and let $L \in V^{* *}$ . Put $v = \sum_{i} L (b_{i}^{*}) b_{i}$ . By [L2], every $f \in V^{*}$ is $\sum_{i} f (b_{i}) b_{i}^{*}$ , so $L (f) = \sum_{i} f (b_{i}) L (b_{i}^{*}) = f (v) = J_{V} (v) (f)$ . Thus $L = J_{V} (v)$ and $J_{V}$ is surjective.

L2algebra

1.2

Conversely, suppose $V$ is infinite-dimensional. By [L5], choice supplies a basis $B$ of $V$ , necessarily infinite. Let $Φ = span {b^{*} : b \in B}$ ; [L3] makes $Φ$ proper, so choose $ϕ \in V^{*} ∖ Φ$ . By [L4] applied inside $V^{*}$ , choose $L \in V^{* *}$ with $L ∣_{Φ} = 0$ and $L (ϕ) = 1$ .

L3L4L5givenchoose

2.1

If $L = J_{V} (v)$ , then $b^{*} (v) = J_{V} (v) (b^{*}) = L (b^{*}) = 0$ for every $b \in B$ . All basis coordinates of $v$ vanish, so $v = 0$ ; then $L = J_{V} (0) = 0$ , contradicting $L (ϕ) = 1$ . Hence $L$ is not in the image and $J_{V}$ is not surjective.

step 1.2algebra

3.1

Step 1.1 proves the forward finite-dimensional case and steps 1.2–2.1 prove its contrapositive. Therefore surjectivity is equivalent to finite dimensionality; [L1] additionally shows the finite-dimensional map is an isomorphism.

step 1.1step 1.2step 2.1L1∎

Depends on

Used by

For the polynomial space F[x], the canonical map to the algebraic double dual is injective but not surjective Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

K. Conrad, Infinite-Dimensional Dual Spaces, Corollary 2 (standard reference, not scraped)

Assuming choice, JV:V→V∗∗JV​:V→V∗∗ is surjective if and only if VV is finite-dimensional