TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

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.

Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism

Statement

Let $V$ be a vector space over a field $F$ and $k \geq 0$ . The basic wedge map $\land : V^{k} \to Λ^{k} V$ , $(v_{1}, \dots, v_{k}) \mapsto v_{1} \land \dots \land v_{k}$ , is $k$ -linear and alternating. For every $F$ -vector space $W$ and every alternating $k$ -linear map $f : V^{k} \to W$ of Alternating $k$ -linear maps, there is a unique linear map $\overline{f} : Λ^{k} V \to W$ with

$\overline{f} (v_{1} \land \dots \land v_{k}) = f (v_{1}, \dots, v_{k}) .$

Moreover, if $U$ is a vector space and $\land^{'} : V^{k} \to U$ is a $k$ -linear alternating map with the same property, then there is a unique linear isomorphism $u : Λ^{k} V \to U$ with $u \circ \land = \land^{'}$ .

Facts & Assumptions

Given: A field $F$ , a vector space $V$ , an integer $k \geq 0$ , a vector space $W$ , and an alternating $k$ -linear map $f : V^{k} \to W$ .

[L1]

An alternating $k$ -linear map vanishes whenever two arguments are equal (Alternating $k$ -linear maps).

[L2]

The exterior power is $Λ^{k} V = V^{\otimes k} / W_{k}$ , and the wedge is the universal multilinear map composed with the quotient projection (The $k$ th exterior power as the tensor-power quotient by repeated-vector relations).

[L3]

The iterated tensor product represents $k$ -linear maps: every $k$ -linear map out of $V^{k}$ factors uniquely through the pure-tensor map (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[L4]

A linear map out of $V$ factors uniquely through $V / W$ when it kills $W$ (Universal property of the quotient vector space).

[L5]

Two pairs representing the same class of maps are related by a unique isomorphism carrying structure maps to structure maps (Tensor products are unique up to a unique isomorphism carrying elementary tensors to elementary tensors).

Proof

technique · direct

1.1L1L2L3

The wedge is multilinear and alternating: by [L2] it is the composition of the universal multilinear map of [L3] with the quotient projection, and the projection kills every pure tensor with a repeated pair, which is exactly the vanishing condition of [L1].

1.2L3

Since $f$ is $k$ -linear, [L3] supplies a unique linear map $\tilde{f} : V^{\otimes k} \to W$ with $\tilde{f} (v_{1} \otimes \dots \otimes v_{k}) = f (v_{1}, \dots, v_{k})$ .

2.1L1step 1.2

The map $\tilde{f}$ kills $W_{k}$ : each generator is a pure tensor with a repeated pair, on which $\tilde{f}$ agrees with the alternating map $f$ , which vanishes by [L1]; hence $\tilde{f}$ vanishes on the whole span $W_{k}$ .

3.1L2L4step 1.2step 2.1

By [L4], $\tilde{f}$ factors uniquely through the quotient of [L2], giving a unique linear $\overline{f} : Λ^{k} V \to W$ with the displayed value on every wedge.

4.1step 3.1L5

For the uniqueness up to unique isomorphism, apply the universal property of $(Λ^{k} V, \land)$ to $\land^{'}$ and that of $(U, \land^{'})$ to $\land$ , obtaining $u : Λ^{k} V \to U$ and $v : U \to Λ^{k} V$ with $u \land = \land^{'}$ and $v \land^{'} = \land$ . Then $v u \land = \land$ and $u v \land^{'} = \land^{'}$ , so the uniqueness clause of step 3.1 forces $v u = id$ and $u v = id$ ; this is the two-application argument of [L5].

5.1step 1.1step 3.1step 4.1∎

Steps 1.1 and 3.1 prove the representing property, and step 4.1 the uniqueness of the representing pair.

Depends on

Used by

Dependency tree · two levels

12 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

Keith Conrad, Exterior Powers (standard reference, not scraped)