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.

Symmetrization and alternation are projections

Statement

For each $k$ , the operators $Sym$ and $Alt$ on covariant $k$ -tensors satisfy

${Sym}^{2} = Sym, {Alt}^{2} = Alt .$

Their images are exactly the symmetric and alternating covariant tensors.

Facts & Assumptions

Given: A covariant $k$ -tensor $T$ .

[F1]

Symmetrization and alternation are the normalized averages over $S_{k}$ , with and without the sign factor (Symmetrization and alternation operators).

Proof

technique · direct

1.1

Applying $Sym$ twice gives a double average over $S_{k} \times S_{k}$ . Reindex by the product permutation $ρ = σ τ$ ; each $ρ$ occurs exactly $k!$ times, so the second averaging changes nothing. Thus $Sym (Sym T) = Sym T$ .

F1givenalgebra

1.2

The same reindexing works for $Alt$ , and the sign factors multiply to $sgn (σ τ)$ . Hence $Alt (Alt T) = Alt T$ .

F1givenalgebra

2.1

If $T$ is symmetric, every summand in [F1] equals $T$ , so $Sym T = T$ . Conversely, $Sym T$ is fixed by every permutation because averaging over the whole group is permutation-invariant. The alternating case is identical, with the sign picked up under permutation.

F1step 1.1step 1.2

3.1

Therefore $Sym$ and $Alt$ are projections onto the symmetric and alternating tensors.

step 1.1step 1.2step 2.1∎

Depends on

Symmetrization and alternation operators

Used by

A tensor is not determined by its values on diagonal tuples without symmetry False statement
Symmetric and alternating images are smooth subbundles Theorem

Dependency tree · two levels

3 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

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)