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.

Exterior-power duality pairing

Statement

The canonical pairing

$⟨ ω, v_{1} \land \dots \land v_{k} ⟩ : = ω (v_{1}, \dots, v_{k})$

extends to a nondegenerate bilinear pairing

$⋀^{k} V^{*} \times ⋀^{k} V \to R,$

and for decomposable elements one has

$⟨ α_{1} \land \dots \land α_{k}, v_{1} \land \dots \land v_{k} ⟩ = \det (α_{i} (v_{j})) .$

Facts & Assumptions

Given: Covectors $α_{1}, \dots, α_{k}$ and vectors $v_{1}, \dots, v_{k}$ in a finite-dimensional real vector space $V$ .

[F1]

A decomposable $k$ -vector is the functional $ω \mapsto ω (v_{1}, \dots, v_{k})$ on alternating $k$ -covectors (The finite-dimensional exterior power of vectors).

[F2]

The wedge product is the signed shuffle sum on alternating covectors (The wedge product of alternating covectors).

[L1]

Wedges of a basis and of its dual basis give dual coordinate systems on exterior powers (Wedge monomials in a dual basis form a basis).

Proof

technique · direct

1.1

By [F2], $(α_{1} \land \dots \land α_{k}) (v_{1}, \dots, v_{k})$ is the alternating sum over permutations of $\prod_{i} α_{i} (v_{σ (i)})$ , which is exactly the determinant of the matrix $(α_{i} (v_{j}))$ . By [F1], this is the value of the pairing on the displayed decomposable elements.

F1F2givenalgebra

2.1

Choose a basis $e_{1}, \dots, e_{n}$ of $V$ with dual basis $e^{1}, \dots, e^{n}$ . By [L1], the wedges $e^{I}$ form a basis of $⋀^{k} V^{*}$ and the wedges $e_{I}$ form a basis of $⋀^{k} V$ , and step 1.1 shows $⟨ e^{I}, e_{J} ⟩ = δ_{I J}$ . Therefore the pairing matrix in these bases is the identity, so the pairing is nondegenerate.

L1step 1.1choosealgebra

3.1

Thus the canonical exterior-power pairing is bilinear, has the determinant formula on decomposables, and is nondegenerate.

step 1.1step 2.1∎

Depends on

Used by

The volume coordinate expression changes sign under a reflection Counterexample
Determinant as the pairing of top exterior powers Example
The top exterior power is one-dimensional Proposition

Dependency tree · two levels

19 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)