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.
FALSE: is canonically a subspace of over every field
Statement
For every field , every -vector space , and every , the th exterior power is canonically a linear subspace of the -fold tensor power : the antisymmetrization map
is a well-defined injective linear section of the quotient map , for every field .
Facts & Assumptions
Given: A field , a vector space with , the quotient map , and the antisymmetrization .
The exterior power is the quotient with quotient map (The th exterior power as the tensor-power quotient by repeated-vector relations).
Permuting the entries of a wedge multiplies it by the permutation sign (Exterior multiplication is well defined, graded, associative, unital, and graded-commutative).
Refutation
By [L1], is a quotient of , and the structure map is a surjection with nonzero kernel: for and , extend a nonzero vector to a basis ; then the pure tensor (with the tail omitted when ) is nonzero yet of it is because the first two entries repeat, so the canonical construction presents as a quotient, not a subspace.
For the formula-defined antisymmetrization, [L2] gives
[L2, algebra]
Over a field whose characteristic divides , step 1.2 gives , while by the hypothesis ; a section must satisfy , so is not a section over such a field. The concrete witness is , , : and of that is .
Step 2.1 gives a field , a vector space , and a degree for which the displayed formula is not a section of , so the universal claim "for every field" is false.
Depends on
Used by
Nothing in the library uses this result yet.
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)