Alphabeta Math
Pipeline-generated
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.

18 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 16 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Exterior Powers, Orientation and Hodge Duality

1 · Prerequisites

2 · Summary

Iterated tensor products and their basis and functoriality theorems supply the construction machinery; determinants, linear bases, dimension, and linear independence supply the counting and independence tools; and the published inner-product infrastructure — orthonormal bases, Gram determinants, adjoints, and orthogonal operators — supplies the metric half.

The page builds the exterior powers ΛkV as quotients of the tensor powers by the repeated-vector relations, never dividing by k!, and proves the universal property, the increasing-wedge bases, the dimension and vanishing formulas, and the independence test for a decomposable wedge. It then assembles the graded exterior algebra with its associativity and graded-commutativity laws, proves functoriality, computes the matrix of ΛkT as the signed minor matrix, and derives the determinant action on the top exterior power and determinant multiplicativity. Orientation is defined through the sign of change-of-basis determinants, and the determinant sign detects orientation change. On a finite-dimensional real inner product space the Gram pairing is defined on exterior powers and proved positive definite, the oriented unit volume form and the Hodge star are introduced, and the star is shown to exist uniquely with its orthonormal-basis formula, to be an isometry, and to square to (1)k(nk). Interior product is the adjoint of exterior multiplication, satisfies the graded anticommutation identity, and in oriented Euclidean three-space recovers the cross product as (uv).

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Alternating k-linear maps

Definition

Let F be a field and let V,W be F-vector spaces (Vector space over a field). For k0, a map

f:VkW

is k-linear (multilinear) when it is linear in each of its k arguments separately, with the other arguments held fixed. It is alternating when

f(v1,,vk)=0whenever vi=vj for some 1i<jk.

For k=0, a 0-linear map is a choice of one element of W; for k=1, a 1-linear map is a linear map. Both are alternating vacuously, because there is no pair of arguments to compare.

Remarks

When 20 in F, alternation is equivalent to the sign rule f(,vi,,vj,)=f(,vj,,vi,): expand f(,vi+vj,,vi+vj,)=0 and use 20. In characteristic two the sign rule collapses to the tautology x=x and does not imply alternation; the published witness is Over Z/2, an antisymmetric bilinear form need not be alternating. This page therefore works directly with the repeated-argument condition, never with a division by k!.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The kth exterior power as the tensor-power quotient by repeated-vector relations

Definition

Let V be a vector space over a field F and let k0. The k-fold tensor power is V0=F, V1=V, and for k2 the iterated tensor product of k copies of V under any parenthesization. By Finite iterated tensor products represent multilinear maps independently of parenthesization every parenthesization represents the k-linear maps out of Vk, and different parenthesizations are joined by the unique isomorphism preserving pure tensors, so Vk is determined up to that isomorphism.

Let WkVk be the subspace spanned by all pure tensors v1vk for which vi=vj for some pair 1i<jk (so W0=W1=0). The kth exterior power of V is the quotient vector space

ΛkV:=Vk/Wk,

and the basic wedge map is

:VkΛkV,(v1,,vk)v1vk+Wk.

Remarks

The construction never divides by k!, so ΛkV is defined in every characteristic. Its relation to the Alternating k-linear maps maps is the universal property of Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism; the convention fixed here is that a repeated entry makes the wedge zero.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Decomposable k-vectors and the basic wedge product

Definition

For v1,,vkV, the image of the basic wedge map of The kth exterior power as the tensor-power quotient by repeated-vector relations is written

v1vk:=v1vk+WkΛkV,

and is called the wedge (or exterior product) of the list. A k-vector αΛkV is decomposable (or pure) when it equals v1vk for some list; a general element of ΛkV is a finite sum of decomposables, because the pure tensors span Vk and their classes span the quotient.

For k=0 the empty wedge is 1F=Λ0V; for k=1 the wedge of a single vector is the vector itself under the identification Λ1V=V.

Remarks

The wedge of v1,,vk depends on the order of the list only up to a sign (see Exterior multiplication is well defined, graded, associative, unital, and graded-commutative); the notation v1vk records the order.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The graded exterior algebra ΛV

Definition

The exterior algebra of V is the graded vector space

ΛV:=k0ΛkV=Λ0VΛ1VΛ2V,

whose homogeneous piece of degree k is the exterior power of The kth exterior power as the tensor-power quotient by repeated-vector relations. On decomposables of Decomposable k-vectors and the basic wedge product define the wedge product

(v1vk)(w1w):=v1vkw1wΛk+V,

and extend bilinearly to all of ΛkV×ΛV. The product of two homogeneous elements is homogeneous of the sum of the degrees, so ΛV is a graded algebra with unit 1F=Λ0V.

The product is well defined. Each generator v1vk of Wk contains a repeated pair, so its concatenation with any pure tensor of degree lies in Wk+. By linearity, concatenation sends Wk×V and Vk×W into Wk+. It therefore descends to a bilinear map on the two quotient spaces, and that descended map is exactly the displayed wedge product. Associativity and the graded commutation law are proved in Exterior multiplication is well defined, graded, associative, unital, and graded-commutative.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

The induced map ΛkT on exterior powers

Definition

Let T:VW be linear. Iterating the induced map of Module homomorphisms induce tensor-product homomorphisms functorially gives the k-fold tensor power

Tk:VkWk,Tk(v1vk)=T(v1)T(vk),

with T0=idF and T1=T. A pure tensor with vi=vj maps to the pure tensor with T(vi)=T(vj), so Tk(Wk(V))Wk(W) for the relation subspaces of The kth exterior power as the tensor-power quotient by repeated-vector relations. Hence Tk descends to the quotient, defining the kth exterior power

ΛkT:ΛkVΛkW,ΛkT(v1vk)=T(v1)T(vk).

For k=0 this is Λ0T=idF, and for k=1 it is T itself under Λ1V=V.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Orientation of a finite-dimensional real vector space

Definition

Let V be a finite-dimensional real vector space (Finite-dimensional vector space, and its dimension dimFV; infinite-dimensional means having no finite basis). Two ordered bases B,B of V (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) are declared equivalent when the determinant of the unique change-of-basis linear isomorphism P:VV carrying B to B satisfies detP>0, where the determinant is The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and 1 on the zero space and positivity is the order of the real field The reals form a totally ordered field.

This is an equivalence relation. The identity change of basis has determinant 1>0. If BB through P, then BB through P1, and det(P1)=(detP)1>0. If BBB through P,Q, then det(QP)=detQdetP>0 by For same-sized finite square matrices over a commutative ring, det(AB)=det(A)det(B).

An orientation of V is an equivalence class of ordered bases under this relation; a basis in the chosen class is positively oriented for that orientation. When dimV1 there are exactly two orientations: fixing one ordered basis B0, every other basis B has detP>0 or detP<0 by the trichotomy of The reals form a totally ordered field. If dimV=1, replacing the sole basis vector of B0 by its negative produces a basis with determinant 1; if dimV2, interchanging two entries of B0 does the same. Thus both classes occur. When dimV=0 the only ordered basis is the empty one and there is exactly one orientation.

Remarks

Orientations depend only on the real vector-space structure; no inner product or basis preference enters the definition.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

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 k0. The basic wedge map :VkΛkV, (v1,,vk)v1vk, is k-linear and alternating. For every F-vector space W and every alternating k-linear map f:VkW of Alternating k-linear maps, there is a unique linear map f:ΛkVW with

f(v1vk)=f(v1,,vk).

Moreover, if U is a vector space and :VkU is a k-linear alternating map with the same property, then there is a unique linear isomorphism u:ΛkVU with u=.

Facts & Assumptions

Given: A field F, a vector space V, an integer k0, a vector space W, and an alternating k-linear map f:VkW.

[L1]

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

[L2]

The exterior power is ΛkV=Vk/Wk, and the wedge is the universal multilinear map composed with the quotient projection (The kth 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 Vk 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.1

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].

L1L2L3
1.2

Since f is k-linear, [L3] supplies a unique linear map f~:VkW with f~(v1vk)=f(v1,,vk).

L3
2.1

The map f~ kills Wk: each generator is a pure tensor with a repeated pair, on which f~ agrees with the alternating map f, which vanishes by [L1]; hence f~ vanishes on the whole span Wk.

L1step 1.2
3.1

By [L4], f~ factors uniquely through the quotient of [L2], giving a unique linear f:ΛkVW with the displayed value on every wedge.

L2L4step 1.2step 2.1
4.1

For the uniqueness up to unique isomorphism, apply the universal property of (ΛkV,) to and that of (U,) to , obtaining u:ΛkVU and v:UΛkV with u= and v=. Then vu= and uv=, so the uniqueness clause of step 3.1 forces vu=id and uv=id; this is the two-application argument of [L5].

step 3.1L5
5.1

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

step 1.1step 3.1step 4.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The basic wedge map (v1,,vk)v1vk is multilinear and alternating

Statement

For every k0, the map

(v1,,vk)v1vk

from Vk to ΛkV is k-linear and alternating, in the sense of Alternating k-linear maps.

Facts & Assumptions

Given: A vector space V over a field F and k0.

[L1]

The exterior power is the quotient ΛkV=Vk/Wk, and the basic wedge map is the universal multilinear map composed with the quotient projection (The kth exterior power as the tensor-power quotient by repeated-vector relations).

[L2]

The wedge map represents alternating k-linear maps and is itself k-linear and alternating (Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism).

Proof

technique · direct
1.1

By [L1], the wedge of Decomposable k-vectors and the basic wedge product is obtained from the universal multilinear map by a linear quotient map, so it is linear in each of its k arguments.

L1
1.2

By [L1], the quotient projection sends every pure tensor with a repeated pair to zero, so the wedge vanishes whenever two arguments are equal.

L1
2.1

Steps 1.1 and 1.2 are exactly multilinearity and alternation; they match the structure map described in [L2], whose universal property supplies the same statements.

step 1.1step 1.2L2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Increasing-index wedges of a basis form a basis of ΛkV

Statement

Let V have the ordered basis (e1,,en) over F and let 0kn. For each k-element subset I={i1<<ik}{1,,n} write

eI:=ei1eik.

Then the family (eI)I indexed by the k-element subsets of {1,,n} is a basis of ΛkV.

Facts & Assumptions

Given: A vector space V with ordered basis (e1,,en) and a degree 0kn.

[L1]

The exterior power is ΛkV=Vk/Wk with the wedge equal to the universal multilinear map composed with the quotient projection (The kth exterior power as the tensor-power quotient by repeated-vector relations).

[L2]

The pure tensors ei1eik over all k-tuples form a basis of Vk (The elementary tensors of two bases form the product basis of the tensor product).

[L3]

Alternating k-linear maps factor uniquely through ΛkV (Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism).

[L5]

For k1, the matrix determinant is alternating and multilinear in the columns, with det(Ik)=1 (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

Proof

technique · direct
1.1

If k=0, then [L1] gives Λ0V=F, and the unique 0-element subset of {1,,n} is , with e:=1F a basis of F. So only the case k1 remains.

L1
1.2

Assume k1. By [L2], every element of Vk is a linear combination of the pure tensors over all k-tuples; passing to the quotient of [L1], every element of ΛkV is a linear combination of the wedges ei1eik over all k-tuples.

L1L2
1.3

Still assuming k1, a wedge with a repeated index is zero by [L1], and a wedge with distinct indices equals the increasing-index wedge up to a sign: transposing two adjacent wedge entries multiplies the wedge by 1, because by [L1] the alternating relation gives 0=(v+wv+w)=(vw)+(wv).

L1algebra
1.4

For each k-subset J={j1<<jk} define φJ:VkF by φJ(v1,,vk):=detM, where M is the k×k matrix whose rth column is the list of the j1,,jk coordinates of vr; by [L5], φJ is k-linear and alternating, so [L3] induces a unique linear map φJ:ΛkVF with φJ(v1vk)=φJ(v1,,vk).

L3L5
2.1

If k1, then steps 1.2 and 1.3 give that the increasing wedges eI span ΛkV.

step 1.2step 1.3L4
2.2

If k1, then for subsets I,J, the matrix for φJ at (ei1,,eik) is the identity when I=J and has a zero row when IJ, so [L5] and step 1.4 give φJ(eI)=1 for I=J and 0 for IJ.

L5step 1.4
3.1

If k1 and IcIeI=0, applying φJ of step 1.4 gives cJ=0 for every J by step 2.2, so the increasing wedges are linearly independent in the sense of [L4].

step 1.4step 2.2L4
4.1

Step 1.1 handles k=0, while steps 2.1 and 3.1 show that for k1 the increasing wedges are a spanning independent set. Therefore in every case the family (eI)I is a basis of ΛkV.

step 1.1step 2.1step 3.1L4
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

If dimV=n, then dimΛkV=(nk)

Statement

If V is finite-dimensional over F with dimV=n, then for every 0kn,

dimΛkV=(nk).

Facts & Assumptions

Given: A finite-dimensional vector space V with dimV=n.

[L1]

The increasing-index wedges of an ordered basis form a basis of ΛkV, indexed by the k-element subsets (Increasing-index wedges of a basis form a basis of ΛkV).

[L2]

The dimension of a finite-dimensional vector space is the size of any of its bases (Finite-dimensional vector space, and its dimension dimFV; infinite-dimensional means having no finite basis).

[L3]

The binomial coefficient is (nk)=[n]k, the number of k-element subsets of an n-element set (The set [A]k of k-element subsets and the binomial coefficient (nk):=[n]k).

Proof

technique · direct
1.1

Since dimV=n, there is an ordered basis (e1,,en) of V by [L2].

L2
2.1

By [L1], the set of wedges eI over the k-element subsets I of {1,,n} is a basis of ΛkV.

L1step 1.1
3.1

By [L3] there are exactly (nk) such subsets, and by [L2] the dimension equals that count.

L2L3step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

If k>dimV, then ΛkV=0

Statement

If V is finite-dimensional with dimV=n and k>n, then ΛkV=0.

Facts & Assumptions

Given: A finite-dimensional vector space V with dimV=n and a degree k>n.

[L1]
[L3]

In a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent (In a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent).

[L4]

The exterior power ΛkV is the quotient of Vk generated by decomposable wedges v1vk (The kth exterior power as the tensor-power quotient by repeated-vector relations).

Proof

technique · direct
1.1

If some k-tuple (v1,,vk) in V were linearly independent, then its image set would be a linearly independent subset of V with k elements. That contradicts [L1] and [L2] because k>n. So every k-tuple in V is linearly dependent.

L1L2algebra
2.1

By [L3], step 1.1 forces every decomposable wedge v1vk to vanish.

L3step 1.1
3.1

By [L4], every element of ΛkV is a linear combination of decomposable wedges, so step 2.1 forces every element of ΛkV to be zero.

L4step 2.1
4.1

Hence ΛkV=0 whenever k>n.

step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

In a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent

Statement

Let V be a finite-dimensional vector space over F. For v1,,vkV,

v1vk0v1,,vk are linearly independent.

Facts & Assumptions

Given: A finite-dimensional vector space V over a field F and a finite list v1,,vk.

[L2]

The increasing-index wedges of a basis form a basis of ΛkV (Increasing-index wedges of a basis form a basis of ΛkV).

[L3]

In a finite-dimensional vector space, every linearly independent subset is contained in a basis, with no choice principle needed (If dimFV=n and U is a linear subspace of V, then U is finite-dimensional, dimFUn, and dimFU=n if and only if U=V).

Proof

technique · direct
1.1

If v1,,vk are dependent, choose by [L1] an entry vj=ijcivi. Expanding the wedge by the multilinearity of the wedge map gives v1vk=ijci(v1vivk) with vi in the jth slot, and every summand has the repeated entry vi, so alternation kills it; hence the wedge is zero.

L1algebra
1.2

If v1,,vk are independent, [L3] places the subset {v1,,vk} inside a basis of V; ordering the remaining basis vectors after v1,,vk gives a basis (v1,,vk,uk+1,,un) of V. Then v1vk is the basis wedge attached to the first k indices, so by [L2] it is a basis vector and in particular nonzero.

L2L3
2.1

Steps 1.1 and 1.2 prove the two directions of the equivalence.

step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

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 1F=Λ0V, is graded in the sense that ΛkVΛVΛk+V, and is graded-commutative:

αβ=(1)kβα(αΛkV, βΛ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).

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.

L1
1.2

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

L1
1.3

Associativity: on decomposables, (αβ)γ and α(βγ) 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=vw+wv, so vw=wv; no division by 2 is used, so this holds in characteristic two as well, where it reads vw=wv.

L2algebra
2.1

Block swap: for decomposable α=v1vk and β=w1w, move each of the factors wj leftward past all k factors vi using step 1.4, collecting k factors of 1; associativity of step 1.3 makes the block move legitimate, giving αβ=(1)kβα, 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
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Exterior powers are functorial

Statement

For linear maps T:VW and S:WU and every k0, the induced maps of The induced map ΛkT on exterior powers satisfy

Λk(idV)=idΛkV,Λk(ST)=ΛkSΛkT.

Thus VΛkV, TΛkT is a functor from F-vector spaces to F-vector spaces, for each fixed k.

Facts & Assumptions

Given: Linear maps T:VW and S:WU and a degree k0.

[L1]

The induced map is ΛkT(v1vk)=T(v1)T(vk) (The induced map ΛkT on exterior powers).

[L2]

A linear map out of ΛkV is determined by its values on decomposable wedges, by the uniqueness clause of the universal property (Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism).

Proof

technique · direct
1.1

By [L1], Λk(idV)(v1vk)=v1vk, so it agrees with idΛkV on decomposables; [L2] then gives equality everywhere.

L1L2
1.2

By [L1] applied to ST and to each factor, Λk(ST)(v1vk)=S(T(v1))S(T(vk))=ΛkS(T(v1)T(vk))=(ΛkSΛkT)(v1vk); [L2] extends the equality from decomposables to all of ΛkV.

L1L2
2.1

Steps 1.1 and 1.2 are the identity and composition laws of a functor, with the k=0 and k=1 cases the conventions of [L1].

step 1.1step 1.2L1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

In basis-wedge coordinates, the matrix of ΛkT is the signed matrix of k-minors

Statement

Let V,W be finite-dimensional with ordered bases (e1,,en) and (f1,,fm), let T:VW be linear with matrix A=(aij), so T(ej)=iaijfi, and let 1kmin(n,m). In the wedge bases (eI) and (fJ) of Increasing-index wedges of a basis form a basis of ΛkV, the matrix of ΛkT has entries

[ΛkT]J,I=detAJ,I,

where AJ,I is the k×k submatrix of A with rows J={j1<<jk} and columns I={i1<<ik}.

Facts & Assumptions

Given: Ordered bases, a linear map T with matrix A, and k-subsets I,J.

[L1]

The induced map is ΛkT(eI)=T(ei1)T(eik) (The induced map ΛkT on exterior powers).

[L2]

The jth column of A is the coordinate column of T(ej), i.e. T(ej)=iaijfi (Coordinate columns [v]B and matrices [T]BC of linear maps relative to ordered bases).

[L3]

The wedge families (eI) and (fJ) are bases of the exterior powers (Increasing-index wedges of a basis form a basis of ΛkV).

[L4]

The matrix determinant is the Leibniz sum detB=σsgn(σ)rbσ(r),r (For n1, the determinant over a commutative ring by the Leibniz formula, and detA for a real matrix).

Proof

technique · direct
1.1

By [L1], ΛkT(eI)=T(ei1)T(eik).

L1
1.2

By [L2], each factor expands as T(eir)=mam,irfm.

L2
1.3

By [L3], the wedges fJ form a basis of ΛkW.

L3
2.1

Expanding step 1.1 with step 1.2 and collecting the coefficient of fJ=fj1fjk: only tuples with distinct indices survive (a repeated index makes the wedge zero), and reordering the tuple into increasing order multiplies by the permutation sign, so the coefficient is σSksgn(σ)ajσ(1),i1ajσ(k),ik, which is detAJ,I by [L4].

step 1.1step 1.2L4algebra
3.1

By step 1.3 and [L2], the coefficients computed in step 2.1 are exactly the entries of the matrix of ΛkT in the wedge bases.

step 1.3step 2.1L2
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

On ΛnV, the induced map ΛnT is multiplication by detT

Statement

Let T:VV be an endomorphism of a finite-dimensional vector space of dimension n1. Then ΛnV is one-dimensional with basis e1en for any ordered basis (e1,,en), and

ΛnT=det(T)idΛnV.

For n=0, Λ0T=idF=det(T)idF by convention.

Facts & Assumptions

Given: An endomorphism T of an n-dimensional vector space V, n1, and an ordered basis B=(e1,,en).

[L1]

The matrix of ΛnT in the top wedge basis has the single entry detA[n],[n]=detA (In basis-wedge coordinates, the matrix of ΛkT is the signed matrix of k-minors).

Proof

technique · direct
1.1

By [L1] with k=n, the wedge basis of ΛnV is the single vector e1en, so ΛnV is one-dimensional and the matrix of ΛnT is the 1×1 matrix with entry detA.

L1
1.2

By [L2], that entry is det(T).

L2
2.1

Hence ΛnT(e1en)=det(T)(e1en), and one-dimensionality makes ΛnT=det(T)id.

step 1.1step 1.2
3.1

For every decomposable top wedge v1vn, one has v1vn=c(e1en) for a unique scalar c by step 1.1, so step 2.1 gives

ΛnT(v1vn)=cΛnT(e1en)=det(T)(v1vn).

[step 1.1, step 2.1, algebra]

4.1

Steps 2.1 and 3.1 establish the claimed scalar action in positive dimension, and the conventions cover n=0.

step 2.1step 3.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Determinant multiplicativity follows from the top exterior power

Statement

For endomorphisms S,T of an n-dimensional vector space V with n1,

det(ST)=det(S)det(T).

Facts & Assumptions

Given: Endomorphisms S,T of an n-dimensional vector space V, n1.

[L1]

The top exterior power acts by the determinant: ΛnT=det(T)id (On ΛnV, the induced map ΛnT is multiplication by detT).

[L2]

Exterior powers preserve composition: Λn(ST)=ΛnSΛnT (Exterior powers are functorial).

Proof

technique · direct
1.1

By [L2], Λn(ST)=ΛnSΛnT.

L2
2.1

Substituting the scalar actions of [L1] gives det(ST)id=det(S)det(T)id on ΛnV.

L1step 1.1
3.1

Since ΛnV is one-dimensional and nonzero, comparing the two scalars gives det(ST)=det(S)det(T).

step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

A real linear isomorphism preserves or reverses orientation according to the sign of its determinant

Statement

Let T:VV be a linear isomorphism of an oriented real vector space with dimV=n1. If detT>0, then T carries every positively oriented basis to a positively oriented basis; if detT<0, then T carries every positively oriented basis to a negatively oriented one. Thus the sign of detT is exactly whether T preserves or reverses the orientation.

Facts & Assumptions

Given: A linear isomorphism T of an oriented n-dimensional real vector space, n1, and a positively oriented ordered basis B.

[L1]

An orientation is an equivalence class of ordered bases, with two bases equivalent exactly when the determinant of their change-of-basis isomorphism is positive; a nonzero real determinant is positive or negative (Orientation of a finite-dimensional real vector space).

[L2]

The top exterior power acts by the determinant: ΛnT=det(T)id (On ΛnV, the induced map ΛnT is multiplication by detT).

Proof

technique · direct
1.1

Fix a positively oriented ordered basis B=(b1,,bn); the transported list T(B)=(T(b1),,T(bn)) is again an ordered basis because T is an isomorphism, and the change-of-basis map from B to T(B) is T itself.

givenL1
1.2

By [L1], T(B) is positively oriented exactly when detT>0, and negatively oriented exactly when detT<0; both cases are exhaustive because T invertible has detT0.

L1
2.1

The top exterior action of [L2] records the same sign: T(b1)T(bn)=ΛnT(b1bn)=det(T)b1bn, so the transported basis belongs to the class of B precisely when the scalar is positive.

L2step 1.1
3.1

Steps 1.2 and 2.1 prove both the preservation and the reversal claims, and the orientation class of the transported basis is independent of the positively oriented basis chosen.

step 1.2step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

The Gram inner product on ΛkV

Definition

Let V be a finite-dimensional real inner product space (Real and complex inner product spaces, with the inner product linear in the first argument) and k0. On decomposable wedges of The kth exterior power as the tensor-power quotient by repeated-vector relations put

v1vk, w1wk:=det(vi,wj)i,jk,

the determinant (For n1, the determinant over a commutative ring by the Leibniz formula, and detA for a real matrix) of the k×k matrix of pairings. For k=0 both sides are the empty determinant, which is 1.

For each fixed list (w1,,wk), the assignment (v1,,vk)det(vi,wj) is k-linear (each entry is linear in the corresponding vi, and the determinant is multilinear in its rows) and alternating (if vi=vi, two rows of the matrix are equal, so the determinant vanishes). It therefore descends to a linear functional on ΛkV in the first slot, and symmetrically in the second slot. The resulting bilinear pairing is the Gram inner product on ΛkV; that it is an inner product in the sense of Real and complex inner product spaces, with the inner product linear in the first argument is proved in The Gram formula gives a well-defined positive-definite inner product on exterior powers, and v1vk2 is the Gram determinant , which also discharges the well-definedness obligation recorded above.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The Gram formula gives a well-defined positive-definite inner product on exterior powers, and v1vk2 is the Gram determinant

Statement

Let V be a finite-dimensional real inner product space of dimension n, and let 0kn. The formula

v1vk, w1wk=det(vi,wj)i,jk

defines a well-defined inner product on ΛkV in the sense of Real and complex inner product spaces, with the inner product linear in the first argument. In particular, for every list (v1,,vk),

v1vk2=detG(v1,,vk),

the Gram determinant of The Gram matrix G(v0,,vr1)=(vi,vj)i,j<r and Gram determinant, with empty value 1, which vanishes exactly when the list is dependent.

Facts & Assumptions

Given: A finite-dimensional real inner product space V of dimension n, a degree 0kn, and lists of length k in V.

[L1]

The intended pairing is the displayed determinant formula, with descent through the quotient in each slot (The Gram inner product on ΛkV).

[L2]

The Gram matrix is G(v1,,vk)=(vi,vj)i,j, with empty determinant 1 (The Gram matrix G(v0,,vr1)=(vi,vj)i,j<r and Gram determinant, with empty value 1).

[L3]

The Gram determinant is nonnegative, and positive exactly for independent lists (A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent).

[L4]

The increasing-index wedges of an orthonormal basis form a basis of ΛkV (Increasing-index wedges of a basis form a basis of ΛkV).

[L5]

Alternating multilinear maps factor uniquely through ΛkV (Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism).

[L6]

A finite-dimensional inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).

[L7]

The determinant is unchanged by transposition: det(MT)=detM (For every square matrix over a commutative ring, det(AT)=det(A)).

Proof

technique · direct
1.1

For a fixed list (w1,,wk), the assignment (v1,,vk)det(vi,wj) is k-linear and alternating in the v's (determinant multilinear in rows, zero on a repeated row), so by [L5] it descends to a unique linear functional on ΛkV; symmetrically in the second slot. This is the well-defined bilinear pairing of [L1].

L1L5
1.2

By [L1] and [L2], the pure-wedge norm square is v1vk2=detG(v1,,vk).

L1L2
1.3

Symmetry: β,α=det(wj,vi)=det((vi,wj)T)=α,β by [L7].

L2L7
2.1

Choose an orthonormal basis (e1,,en) by [L6]; by [L4] the wedges eI form a basis of ΛkV, and by step 1.2 the pairing satisfies eI,eJ=det of the identity submatrix, which is 1 when I=J and 0 otherwise.

step 1.2L2L4L6
2.2

The norm-square formula of step 1.2 is the claimed Gram-determinant identity, and by [L3] that determinant is nonnegative and vanishes exactly for dependent lists, matching the independence criterion of In a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent.

step 1.2L3
3.1

Expanding α=IcIeI in the basis of step 2.1 gives α,α=IcI20, with equality exactly when every cI=0, i.e. α=0; with steps 1.1 and 1.3 this is a positive-definite inner product.

step 1.1step 1.3step 2.1algebra
4.1

Steps 1.1, 2.2 and 3.1 prove well-definedness, the Gram-determinant formula, and positive definiteness.

step 1.1step 1.2step 2.2step 3.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

The oriented unit volume form

Definition

Let V be an oriented finite-dimensional real inner product space with dimV=n1 (Orientation of a finite-dimensional real vector space). Choose a positively oriented orthonormal basis (b1,,bn), which exists by Every finite-dimensional real or complex inner product space has an orthonormal basis, and define the oriented unit volume form

ω:=b1bnΛnV.

This is independent of the choice. Any other positively oriented orthonormal basis (b1,,bn) is obtained from (b1,,bn) by a linear map Q that carries one orthonormal basis to another, hence is an orthogonal operator by For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and TT=I are equivalent; over the reals its determinant is therefore ±1 by Orthogonal and unitary operators form groups, and their determinants have modulus one. Positivity of the change of basis forces detQ=1, and by On ΛnV, the induced map ΛnT is multiplication by detT,

b1bn=ΛnQ(b1bn)=detQ(b1bn)=ω.

The form is a unit. By the Gram pairing of The Gram formula gives a well-defined positive-definite inner product on exterior powers, and v1vk2 is the Gram determinant, ω,ω=det(bi,bj)=detIn=1. For n=0, set ω:=1Λ0V=R.

Remarks

Reversing the orientation replaces ω by ω; the oriented unit volume form is where the orientation enters the Hodge-star data.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The Hodge star on an oriented finite-dimensional real inner-product space

Definition

Let V be an oriented finite-dimensional real inner product space of dimension n, with Gram pairings on the exterior powers of The Gram inner product on ΛkV and oriented unit volume form ω of The oriented unit volume form. For each degree k with 0kn, the Hodge star

:ΛkVΛnkV

is the linear map characterized by

αβ=α,βωfor all α,βΛkV.

Existence and uniqueness of for every degree 0kn are proved in The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis , which discharges the well-definedness obligation recorded above.

Remarks

The Hodge star needs the metric (through the Gram pairing) and the orientation (through ω); the bare vector-space structure does not determine it. With the opposite orientation ω is replaced by ω, and the star is replaced by .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis

Statement

Let V be an oriented finite-dimensional real inner product space of dimension n. For every degree 0kn there is a unique linear map :ΛkVΛnkV satisfying

αβ=α,βωfor all α,βΛkV,

where ω is the oriented unit volume form of The oriented unit volume form. If (e1,,en) is a positively oriented orthonormal basis and I={i1<<ik} has complement Ic={i1c<<inkc}, let εI be the sign of the permutation (i1,,ik,i1c,,inkc)(1,,n); then

eI=εIeIc.

Facts & Assumptions

Given: An oriented n-dimensional real inner product space V, its unit volume form ω, a degree k, and a positively oriented orthonormal basis (e1,,en).

[L1]

The Hodge star is characterized by αβ=α,βω (The Hodge star on an oriented finite-dimensional real inner-product space).

[L3]

The unit volume form is ω=e1en for the positively oriented orthonormal basis, with ω,ω=1 (The oriented unit volume form).

[L4]

The wedges eI form a basis of ΛkV and the wedges eIc a basis of ΛnkV (Increasing-index wedges of a basis form a basis of ΛkV).

Proof

technique · direct
1.1

By [L3] and [L4], the positively oriented orthonormal basis exists and yields the wedge bases (eI)I of ΛkV and (eJ)J of ΛnkV.

L3L4
2.1

Define a linear map :ΛkVΛnkV by eI:=εIeIc on the basis of step 1.1.

step 1.1
3.1

For subsets I,J of sizes k and k, one has eJeIc=0 unless J=I: if JI some index occurs twice, and if J=I then eIeIc=εIe1en=εIω by the definition of εI and [L3]. The Gram pairing of [L2] on the orthonormal basis satisfies eJ,eI=1 for J=I and 0 otherwise, so eJeI=εIeJeIc=eJ,eIω for all I,J.

L2L3step 1.1step 2.1
4.1

Both sides of the relation of [L1] are bilinear in (α,β), so step 3.1 extends from basis wedges to the identity αβ=α,βω for all α,βΛkV.

step 3.1algebra
5.1

Uniqueness: if also satisfies [L1], then α(ββ)=0 for all α; pairing with ω through the Gram inner product of [L2] gives α,(ββ)=0 for all α, so nondegeneracy forces (ββ)=0; the map of step 2.1 permutes a basis up to sign, hence is bijective, so β=β.

L1L2step 2.1step 4.1
6.1

Steps 2.1 and 4.1 prove existence with the complementary-basis formula, and step 5.1 proves uniqueness.

step 2.1step 4.1step 5.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The Hodge star is an isometry and satisfies 2=(1)k(nk) on ΛkV

Statement

On ΛkV of an oriented n-dimensional real inner product space, the Hodge star preserves the Gram pairing,

α,β=α,β,

and satisfies

=(1)k(nk)idΛkV.

Facts & Assumptions

Given: An oriented n-dimensional real inner product space V, a degree k, and a positively oriented orthonormal basis (e1,,en).

[L1]

In a positively oriented orthonormal basis, eI=εIeIc, where εI is the sign of the permutation listing I followed by its complement (The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis).

Proof

technique · direct
1.1

By [L1], sends the orthonormal wedge basis (eI)I to the family (εIeIc)I, which is the complementary orthonormal wedge basis with signs attached; hence eI,eJ=δI,J=eI,eJ, and bilinearity gives the isometry on all of ΛkV.

L1algebra
1.2

For each I, apply [L1] twice: (eI)=εIeIc=εIεIceI, where εIc is the sign of the permutation listing Ic followed by I. The two permutations differ by interchanging a block of size k with a block of size nk, whose sign is (1)k(nk), so εIc=(1)k(nk)εI and 2eI=(1)k(nk)eI.

L1algebra
2.1

Since the eI form a basis, step 1.2 gives =(1)k(nk)id on ΛkV.

step 1.2
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Interior product on the exterior algebra

Definition

Let V be a finite-dimensional real inner product space and vV. For each degree k1, exterior multiplication by v,

mv:Λk1VΛkV,mv(α)=vα,

is a linear map between finite-dimensional inner product spaces, the target carrying the Gram pairing of The Gram inner product on ΛkV and the wedge product being Exterior multiplication is well defined, graded, associative, unital, and graded-commutative. Its adjoint exists and is unique by Every linear map between finite-dimensional inner product spaces has a unique adjoint. The interior product (contraction) by v is that adjoint:

ιv:=mv:ΛkVΛk1V,ιvα,β=α,vβ,

with ιv=0 on Λ0V. The explicit value of ιv on a decomposable wedge is computed in Interior product is the adjoint of exterior multiplication by a vector , which discharges the well-definedness obligation recorded above.

Remarks

The three defining properties of the interior product — ιv(1)=0, ιv(w)=v,w for wV, and the graded derivation rule of Exterior multiplication and interior product satisfy the graded anticommutation identity — each follow from the adjoint description.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Interior product is the adjoint of exterior multiplication by a vector

Statement

For vV, the interior product ιv of Interior product on the exterior algebra is the adjoint of exterior multiplication mv(α)=vα. On a decomposable wedge,

ιv(v1vk)=r=1k(1)r1v,vrv1vr^vk,

where vr^ means vr is omitted. Equivalently, ιv is the unique linear operator with ιv(1)=0, ιv(w)=v,w for wV, and the graded derivation rule ιv(wα)+wιv(α)=v,wα, established on the following page item as the anticommutation identity.

Facts & Assumptions

Given: A finite-dimensional real inner product space V, a vector v, and a degree k1.

[L1]

The interior product is the adjoint ιv=mv, characterized by ιvα,β=α,vβ (Interior product on the exterior algebra).

[L2]

The wedge product is multilinear, and vw=wv for vectors (Exterior multiplication is well defined, graded, associative, unital, and graded-commutative).

[L3]

A linear map between finite-dimensional inner product spaces has a unique adjoint (Every linear map between finite-dimensional inner product spaces has a unique adjoint).

[L4]

A finite-dimensional inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).

[L5]

A linear map out of ΛkV is determined by its values on decomposable wedges (Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism).

Proof

technique · direct
1.1

The map mv:Λk1VΛkV is linear by [L2], so [L3] supplies its unique adjoint; by [L1] that adjoint is ιv with ιvα,β=α,vβ.

L1L2L3
1.2

Choose an orthonormal basis (e1,,en) by [L4], write v=jvjej, and let I={i1<<ik}. Then ιveI,eJ=eI,veJ=jvjeI,ejeJ, and the pairing is nonzero only when J=I{ir} for some r and j=ir, in which case ejeJ=(1)r1eI.

L2L4algebra
2.1

By step 1.2, ιveI=r=1k(1)r1vireI{ir}, since the eJ form an orthonormal basis of Λk1V and the pairing is nondegenerate by [L1].

step 1.2L1
3.1

The assignment Φv(v1,,vk):=r=1k(1)r1v,vrv1vr^vk is multilinear (each term is multilinear) and alternating (when va=vb, the two terms r=a and r=b cancel by the block sign of [L2], and the remaining terms have a repeated entry), so by [L5] there is a unique linear map agreeing with Φv on decomposables; on the basis wedge eI it equals step 2.1, hence it is ιv.

L2L5step 2.1
4.1

Steps 1.1 and 3.1 prove the adjoint description and the displayed contraction formula; evaluating at k=0,1 gives ιv(1)=0 and ιv(w)=v,w, the two boundary clauses of the characterization.

step 1.1step 3.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Exterior multiplication and interior product satisfy the graded anticommutation identity

Statement

For vectors v,w in a finite-dimensional real inner product space V and every αΛkV,

ιv(wα)+wιv(α)=v,wα.

Facts & Assumptions

Given: Vectors v,wV and an element αΛkV.

[L1]

The interior product is the adjoint of exterior multiplication: ιvα,β=α,vβ (Interior product on the exterior algebra).

[L2]

On a decomposable wedge, ιv(v1vk)=r=1k(1)r1v,vrv1vr^vk (Interior product is the adjoint of exterior multiplication by a vector).

[L3]

The wedge product is bilinear, associative, and satisfies vw=wv for vectors (Exterior multiplication is well defined, graded, associative, unital, and graded-commutative).

Proof

technique · direct
1.1

For a decomposable α=v1vk, apply [L2] to wα=wv1vk: the r=0 term is v,wv1vk, and the terms r1 contribute r=1k(1)r1v,vrwv1vr^vk, because the omission of vr leaves w in position r+1, which costs the sign (1)r.

L2algebra
2.1

Using [L3] to move the leading w and [L2] once more identifies the sum over r1 with wιv(α), so ιv(wα)=v,wαwιv(α).

step 1.1L2L3
3.1

Both sides of the claimed identity are linear in α (the wedge is bilinear by [L3] and ιv is linear by [L1]), so equality extends from decomposables to all of ΛkV.

step 2.1L1L3
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

In oriented Euclidean three-space, the cross product is (uv)

Statement

In R3 with the standard inner product and the standard orientation (the class of the ordered basis (e1,e2,e3)), define the cross product in the oriented orthonormal basis by

u×v:=(u2v3u3v2, u3v1u1v3, u1v2u2v1).

Then u×v=(uv). Equivalently, with the unit volume form ω=e1e2e3, one has u×v=ιvιuω, and u×v is orthogonal to both u and v.

Facts & Assumptions

Given: Vectors u,vR3, the oriented orthonormal basis (e1,e2,e3), and the unit volume form ω.

[L1]

In an oriented orthonormal basis, eI=εIeIc, and the star is characterized by αβ=α,βω (The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis).

[L2]

On Λ2R3, one has 2=id because (1)21=1 (The Hodge star is an isometry and satisfies 2=(1)k(nk) on ΛkV).

[L3]

The interior product contracts by ιv(v1vk)=r=1k(1)r1v,vrv1vr^vk (Interior product is the adjoint of exterior multiplication by a vector).

Proof

technique · direct
1.1

Every bilinear alternating map B:R3×R3R3 is determined by its values on the three pairs (e1,e2),(e2,e3),(e3,e1): expanding in coordinates, B(u,v)=i<j(uivjujvi)B(ei,ej).

algebra
1.2

By [L1], (e1e2)=e3, (e2e3)=e1, and (e3e1)=e2; the map (u,v)(uv) is bilinear and alternating because the wedge is and is linear.

L1algebra
1.3

The coordinate cross product is bilinear and alternating, and satisfies e1×e2=e3, e2×e3=e1, e3×e1=e2.

algebra
2.1

By step 1.1, the two bilinear alternating maps of steps 1.2 and 1.3 agree on the three generating pairs, hence agree everywhere: (uv)=u×v.

step 1.1step 1.2step 1.3
3.1

The interior-product form: by [L3], ιuω=u,e1e2e3u,e2e1e3+u,e3e1e2, and applying ιv to that expansion collects the e1,e2,e3 coordinates u2v3u3v2, u3v1u1v3, u1v2u2v1, so ιvιuω=u×v=(uv) by step 2.1.

L3step 2.1algebra
3.2

Orthogonality: by the defining relation of [L1] and the square law of [L2], u,(uv)ω=u((uv))=uuv=0, and ω0, so u,u×v=0; the same argument with v gives v,u×v=0.

L1L2step 2.1algebra
4.1

Steps 2.1, 3.1 and 3.2 establish the three equivalent descriptions and the orthogonality.

step 2.1step 3.1step 3.2

5 · Examples, counterexamples and false statements

None yet.

Sources