LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Swapping direct summands scales oriented bases by a sign

Statement

Let $U, W$ be oriented finite-dimensional real vector spaces, using determinant-line rays also in dimension zero, with dimensions $k, l$ . The swap $s : U \oplus W \to W \oplus U$ , $s (u, w) = (w, u)$ , has orientation sign $(- 1)^{k l}$ for the written product orientations. If $V = U \oplus W$ is an internal direct sum, the two orientations transported to $V$ by addition likewise differ by $(- 1)^{k l}$ .

Facts & Assumptions

Given: Oriented $U, W$ of dimensions $k, l$ , and, for the internal version, $V = U \oplus W$ .

[F1]

Product orientations use the ordered determinant isomorphism $\det (U \oplus W) ≅ \det U \otimes \det W$ (Product orientations).

[F2]

An orientation is a positive ray in the determinant line, including the two rays in dimension zero (Determinant-line orientations of finite-dimensional real vector spaces).

[F3]

Internal direct sums identify the external sum with $V$ by $(u, w) \mapsto u + w$ (Internal direct sum $V = ⨁_{i < n} U_{i}$ : the sum is everything and each summand meets the sum of the others only in $0_{V}$ ).

Proof

1.1F1F2givenalgebra

For positive-dimensional factors take positive bases $u, w$ . The swap sends the domain's ordered basis $(u, w)$ to the list consisting first of the $U$ -vectors in the second summand, then of the $W$ -vectors in the first. Reordering that image to the codomain's positive list $(w, u)$ takes $k l$ transpositions, so its determinant sign is $(- 1)^{k l}$ . This is the exterior-algebra identity $w \land u = (- 1)^{k l} u \land w$ .

2.1F1F2F3step 1.1algebra∎

The same exterior identity applies to arbitrary positive determinant elements, including signed scalars for a zero-dimensional factor; if $k = 0$ or $l = 0$ its sign is $+ 1$ . For an internal sum, the two addition maps satisfy $a_{W, U} \circ s = a_{U, W}$ , so transporting their product rays to $V$ gives the same comparison sign. Thus both statements hold in every dimension, and for $k = l = 1$ the swap reverses orientation.

Depends on

Used by

A cycle has zero algebraic intersection with a bounding cycle Corollary
Two-map intersection as a diagonal preimage Proposition
Intersection number under factor interchange Theorem

Dependency tree · two levels

13 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

Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall, 1974; complete 236-page PDF) (standard reference, not scraped)