TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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, the canonical map $J_{V} : V \to V^{* *}$ is linear and injective

Statement

Assume the axiom of choice. For every vector space $V$ , the canonical map $J_{V} : V \to V^{* *}$ is linear and injective.

Facts & Assumptions

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

[L1]

The canonical map is defined by $J_{V} (v) (f) = f (v)$ for $v \in V$ and $f \in V^{*}$ (The canonical evaluation map $J_{V} : V \to V^{* *}$ given by $J_{V} (v) (f) = f (v)$ ).

[L2]

If $v \notin U \leq V$ , some functional vanishes on $U$ and takes value $1$ at $v$ (Assuming choice, if $v \notin U \leq V$ , some $f \in V^{*}$ vanishes on $U$ and satisfies $f (v) = 1$ ).

[L3]

A linear map is injective if and only if its kernel is trivial (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial).

Proof

technique · direct

1.1

For $a, b \in F$ , $u, v \in V$ , and $f \in V^{*}$ , [L1] gives $J_{V} (a u + b v) (f) = f (a u + b v) = a J_{V} (u) (f) + b J_{V} (v) (f)$ . Equality at every $f$ proves that $J_{V}$ is linear.

L1algebra

1.2

If $v \neq 0$ , apply [L2] to $U = {0}$ to obtain $f$ with $f (v) = 1$ . Then $J_{V} (v) (f) = 1$ , so $J_{V} (v) \neq 0$ . Hence $\ker J_{V} = {0}$ .

L1L2given

2.1

By [L3], step 1.2 makes $J_{V}$ injective; step 1.1 supplies linearity. The zero space is included, since its unique map has trivial kernel.

step 1.1step 1.2L3∎

Depends on

Used by

Assuming choice, J_V:V→ V^** is surjective if and only if V is finite-dimensional Theorem

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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

Assuming choice, the canonical map JV:V→V∗∗JV​:V→V∗∗ is linear and injective