TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

The graded tensor product for orthogonal sums of quadratic spaces

Statement

Let $k$ be a field of characteristic not $2$ , and let $(V, Q)$ and $(W, R)$ be finite-dimensional quadratic spaces over $k$ , with associated symmetric bilinear forms $B_{Q}, B_{R}$ defined by $B_{Q} (v, v^{'}) = (Q (v + v^{'}) - Q (v) - Q (v^{'})) / 2$ and likewise for $R$ . Give $V \oplus W$ the orthogonal-sum form $(Q \oplus R) (v, w) = Q (v) + R (w)$ . With each Clifford generator odd in the canonical grading of The Clifford quotient has its canonical parity grading, the canonical map

$Φ : C l (V \oplus W, Q \oplus R) ⟶ C l (V, Q) {\hat{\otimes}}_{k} C l (W, R), (v, w) ⟼ \overset{ˉ}{v} \otimes 1 + 1 \otimes \overset{ˉ}{w}$

is an isomorphism of graded $k$ -algebras. No nondegeneracy assumption is needed.

Facts & Assumptions

Given: The field $k$ , finite-dimensional quadratic spaces $(V, Q)$ and $(W, R)$ , and the displayed orthogonal-sum form.

[F1]

In the graded tensor product, homogeneous factors multiply by $(a \otimes b) (a^{'} \otimes b^{'}) = (- 1)^{∣ b ∣ ∣ a^{'} ∣} a a^{'} \otimes b b^{'}$ (Graded algebras, graded modules, and the graded tensor product).

[F2]

In a Clifford algebra the canonical image satisfies ${\overset{ˉ}{v}}^{2} = Q (v) 1$ (Universal Clifford algebra of a quadratic space).

[F3]

A linear map into a unital associative $k$ -algebra satisfying $f (x)^{2} = S (x) 1$ extends uniquely to $C l (X, S)$ (Universal property of the Clifford algebra).

[F4]

If $X$ is finite-dimensional, $\dim_{k} C l (X, S) = 2^{\dim X}$ , including degenerate $S$ (PBW basis and exterior associated graded for a Clifford algebra).

[F5]

Each canonical Clifford generator is odd in the quotient grading (The Clifford quotient has its canonical parity grading).

[F6]

Tensors of basis elements form a basis of the tensor product of finite-dimensional vector spaces (The elementary tensors of two bases form the product basis of the tensor product).

Proof

technique · construct the universal map and compare dimensions

1.1givenF1F2F5algebra

For $v \in V$ and $w \in W$ , set $c (v, w) = \overset{ˉ}{v} \otimes 1 + 1 \otimes \overset{ˉ}{w}$ . Each summand is odd by [F5]. By [F1], $(\overset{ˉ}{v} \otimes 1) (1 \otimes \overset{ˉ}{w}) = \overset{ˉ}{v} \otimes \overset{ˉ}{w}$ and $(1 \otimes \overset{ˉ}{w}) (\overset{ˉ}{v} \otimes 1) = - \overset{ˉ}{v} \otimes \overset{ˉ}{w}$ , so their cross terms cancel in the square. By [F2], the two squares are $Q (v) 1$ and $R (w) 1$ , so $c (v, w)^{2} = (Q (v) + R (w)) 1$ .

2.1givenF3F5step 1.1construct

By [F3], the linear map $(v, w) \mapsto c (v, w)$ extends uniquely to a unital algebra homomorphism $Φ$ with the stated generator values. It preserves parity because every generator maps to an odd element by [F5].

3.1F4F6step 2.1algebra

The image of $Φ$ contains $\overset{ˉ}{v} \otimes 1$ by taking $(v, 0)$ and $1 \otimes \overset{ˉ}{w}$ by taking $(0, w)$ . These elements generate both Clifford factors, and [F4] gives finite bases consisting of products of canonical generators; their elementary tensors span the graded tensor product by [F6]. Thus $Φ$ is surjective.

4.1F4F6step 3.1algebra∎

By [F4], the source has dimension $2^{\dim V + \dim W}$ , and [F6] gives the same dimension for the tensor-product target. A surjective linear map between equal finite-dimensional vector spaces is injective, hence $Φ$ is an isomorphism. This includes either zero-dimensional factor and degenerate forms.

Depends on

Used by

Dependency tree · two levels

20 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

Jean Gallier, Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups, §1.2, Proposition 1.3 (standard reference, not scraped)
M. F. Atiyah, R. Bott, and A. Shapiro, Clifford Modules, Part I, §1, Proposition 1.6 (standard reference, not scraped)