PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Functoriality of finite-dimensional exterior powers

Statement

Let $V, W, X$ be finite-dimensional real vector spaces and let $k \geq 0$ . Every linear map $A : V \to W$ induces a linear map

$⋀^{k} A : ⋀^{k} V \to ⋀^{k} W$

characterized by

$(⋀^{k} A) (v_{1} \land \dots \land v_{k}) = A v_{1} \land \dots \land A v_{k} .$

Moreover,

$⋀^{k} ({id}_{V}) = {id}_{\land^{k} V}, ⋀^{k} (B \circ A) = (⋀^{k} B) \circ (⋀^{k} A) .$

Facts & Assumptions

Given: Finite-dimensional real vector spaces $V, W, X$ , an integer $k \geq 0$ , and linear maps $A : V \to W$ and $B : W \to X$ .

[L1]

Every alternating $k$ -linear map factors uniquely through $⋀^{k} V$ (Universal property of the finite-dimensional exterior power).

Proof

technique · direct

1.1

The map $(v_{1}, \dots, v_{k}) \mapsto A v_{1} \land \dots \land A v_{k}$ is alternating and $k$ -linear in $v_{1}, \dots, v_{k}$ . By [L1], it therefore factors uniquely through a linear map $⋀^{k} A : ⋀^{k} V \to ⋀^{k} W$ with the stated action on decomposable wedges.

L1givenconstruct

2.1

The identity map and the composite $(⋀^{k} B) \circ (⋀^{k} A)$ have the expected values on every decomposable wedge: $⋀^{k} ({id}_{V}) (v_{1} \land \dots \land v_{k}) = v_{1} \land \dots \land v_{k},$ and $((⋀^{k} B) \circ (⋀^{k} A)) (v_{1} \land \dots \land v_{k}) = B A v_{1} \land \dots \land B A v_{k} .$ The same formula holds for $⋀^{k} (B \circ A)$ .

step 1.1givenalgebra

3.1

By uniqueness in [L1], the maps in step 2.1 must agree. Therefore exterior powers preserve identities and composition.

L1step 2.1

4.1

Hence $V \mapsto ⋀^{k} V$ and $A \mapsto ⋀^{k} A$ define a functor.

step 1.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Will J. Merry, Differential Geometry (standard reference, not scraped)