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.
In basis-wedge coordinates, the matrix of is the signed matrix of -minors
Statement
Let be finite-dimensional with ordered bases and , let be linear with matrix , so , and let . In the wedge bases and of Increasing-index wedges of a basis form a basis of , the matrix of has entries
where is the submatrix of with rows and columns .
Facts & Assumptions
Given: Ordered bases, a linear map with matrix , and -subsets .
The induced map is (The induced map on exterior powers).
The th column of is the coordinate column of , i.e. (Coordinate columns and matrices of linear maps relative to ordered bases).
The wedge families and are bases of the exterior powers (Increasing-index wedges of a basis form a basis of ).
The matrix determinant is the Leibniz sum (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
Proof
By [L1], .
By [L2], each factor expands as .
By [L3], the wedges form a basis of .
Expanding step 1.1 with step 1.2 and collecting the coefficient of : 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 , which is by [L4].
By step 1.3 and [L2], the coefficients computed in step 2.1 are exactly the entries of the matrix of in the wedge bases.
Depends on
- The induced map $\Lambda^kT$ on exterior powers
- Increasing-index wedges of a basis form a basis of $\Lambda^kV$
- Coordinate columns $[v]_{\mathcal B}$ and matrices $[T]_{\mathcal B}^{\mathcal C}$ of linear maps relative to ordered bases
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
Used by
Dependency tree · two levels
23 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)