Alphabeta Math
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≥0. Every linear map A:V→W induces a linear map

⋀kA:⋀kV→⋀kW

characterized by

(⋀kA)(v1∧⋯∧vk)=Av1∧⋯∧Avk.

Moreover,

⋀k(id⁡V)=id⁡∧kV,⋀k(B∘A)=(⋀kB)∘(⋀kA).

Facts & Assumptions

Given: Finite-dimensional real vector spaces V,W,X, an integer k≥0, and linear maps A:V→W and B:W→X.

[L1]

Every alternating k-linear map factors uniquely through ⋀kV (Universal property of the finite-dimensional exterior power).

Proof

technique · direct
1.1L1givenconstruct

The map (v1,…,vk)↦Av1∧⋯∧Avk is alternating and k-linear in v1,…,vk. By [L1], it therefore factors uniquely through a linear map ⋀kA:⋀kV→⋀kW with the stated action on decomposable wedges.

2.1step 1.1givenalgebra

The identity map and the composite (⋀kB)∘(⋀kA) have the expected values on every decomposable wedge: ⋀k(id⁡V)(v1∧⋯∧vk)=v1∧⋯∧vk, and ((⋀kB)∘(⋀kA))(v1∧⋯∧vk)=BAv1∧⋯∧BAvk. The same formula holds for ⋀k(B∘A).

3.1L1step 2.1

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

4.1step 1.1step 3.1∎

Hence V↦⋀kV and A↦⋀kA define a functor.

Depends on

Used by

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