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 multiplication is well defined, graded, associative, unital, and graded-commutative

Statement

The wedge product of The graded exterior algebra $Λ V$ is well defined and bilinear in each homogeneous pair of degrees. It is associative, has unit $1 \in F = Λ^{0} V$ , is graded in the sense that $Λ^{k} V \land Λ^{ℓ} V \subseteq Λ^{k + ℓ} V$ , and is graded-commutative:

$α \land β = (- 1)^{k ℓ} β \land α (α \in Λ^{k} V, β \in Λ^{ℓ} V) .$

All of this holds over every field, including characteristic two.

Facts & Assumptions

Given: A vector space $V$ over a field $F$ and homogeneous elements of degrees $k, ℓ$ .

[L1]

The exterior algebra is the graded sum of the exterior powers, with the wedge product defined by concatenation on decomposables and extended bilinearly; the definition checks that a repeated pair persists under concatenation, so the product is well defined (The graded exterior algebra $Λ V$ ).

[L2]

The basic wedge map is multilinear and alternating (The basic wedge map $(v_{1}, \dots, v_{k}) \mapsto v_{1} \land \dots \land v_{k}$ is multilinear and alternating).

Proof

technique · direct

1.1

Well-definedness and bilinearity in each degree pair are recorded in [L1], and the graded containment is the degree count of the concatenation.

1.2

Unitality: for a decomposable $α$ , the convention $1 \land α = α$ is the definition in [L1]; bilinearity extends it.

1.3

Associativity: on decomposables, $(α \land β) \land γ$ and $α \land (β \land γ)$ are both the concatenation of the three lists by [L1]; multilinearity of [L2] extends the equality to all elements.

L1L2

1.4

For vectors $v, w$ , alternation of [L2] applied to $(v + w, v + w)$ gives $0 = v \land w + w \land v$ , so $v \land w = - w \land v$ ; no division by $2$ is used, so this holds in characteristic two as well, where it reads $v \land w = w \land v$ .

L2algebra

2.1

Block swap: for decomposable $α = v_{1} \land \dots \land v_{k}$ and $β = w_{1} \land \dots \land w_{ℓ}$ , move each of the $ℓ$ factors $w_{j}$ leftward past all $k$ factors $v_{i}$ using step 1.4, collecting $ℓ k$ factors of $- 1$ ; associativity of step 1.3 makes the block move legitimate, giving $α \land β = (- 1)^{k ℓ} β \land α$ , and multilinearity extends this to all homogeneous elements.

step 1.3step 1.4L2

3.1

Steps 1.1 through 2.1 prove the five asserted laws in every characteristic, because the only sign rule used is the alternation identity of step 1.4.

step 1.1step 1.2step 1.3step 1.4step 2.1∎

Depends on

Used by

A bivector in ℝ⁴ need not be decomposable Counterexample
Interior product on the exterior algebra Definition
FALSE: ΛᵏV is canonically a subspace of V^⊗ k over every field False statement
Exterior multiplication and interior product satisfy the graded anticommutation identity Proposition
Exterior powers are functorial Theorem
Interior product is the adjoint of exterior multiplication by a vector Theorem

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

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