TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Regrouping two factors: the symmetry decomposition of a two-particle sector over an orbital and an internal factor

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H, V$ be nonzero finite-dimensional complex Hilbert spaces (Hilbert space), $\dim H = m$ , $\dim V = k$ . All tensor products below are the completed tensor products of Hilbert tensor construction: inner product, completion and product bases, with elementary tensors $u \otimes v$ , and all permutation projections $P_{\pm}^{(2)}$ and exchange operators $τ_{W}$ are those of Permutation sector projections on the n-fold tensor power and The two-particle exchange operator and the symmetric and antisymmetric combinations for the displayed Hilbert space $W$ . Then:

(a) identification: the inclusion $κ : H ⊙ V \to H \hat{\otimes} V$ of the algebraic tensor product is a surjective linear isometry, so elementary tensors and finite sums of them may be treated as elements of the completed product without ambiguity; the same holds for $(H \otimes V) \hat{\otimes} (H \otimes V)$ and $(H \otimes H) \hat{\otimes} (V \otimes V)$ ;

(b) regrouping unitary: there is a unique bounded linear operator $Θ : (H \otimes V) \hat{\otimes} (H \otimes V) \to (H \otimes H) \hat{\otimes} (V \otimes V)$ with $Θ ((u \otimes χ) \otimes (v \otimes χ^{'})) = (u \otimes v) \otimes (χ \otimes χ^{'})$ for all $u, v \in H$ , $χ, χ^{'} \in V$ ; $Θ$ is unitary and its inverse is the unique bounded operator with $Θ^{- 1} ((u \otimes v) \otimes (χ \otimes χ^{'})) = (u \otimes χ) \otimes (v \otimes χ^{'})$ ;

(c) exchange intertwining: $Θ τ_{H \otimes V} = (τ_{H} \otimes τ_{V}) Θ$ , where $τ_{H} \otimes τ_{V}$ is the bounded tensor product of the two exchange operators;

(d) symmetriser identities: $Θ P_{-}^{(H \otimes V)} = (P_{-}^{(H)} \otimes P_{+}^{(V)} + P_{+}^{(H)} \otimes P_{-}^{(V)}) Θ$ and $Θ P_{+}^{(H \otimes V)} = (P_{+}^{(H)} \otimes P_{+}^{(V)} + P_{-}^{(H)} \otimes P_{-}^{(V)}) Θ$ ; consequently $Θ$ maps $ran P_{-}^{(H \otimes V)}$ onto the orthogonal direct sum $(ran P_{-}^{(H)} \otimes ran P_{+}^{(V)}) + (ran P_{+}^{(H)} \otimes ran P_{-}^{(V)})$ and $ran P_{+}^{(H \otimes V)}$ onto $(ran P_{+}^{(H)} \otimes ran P_{+}^{(V)}) + (ran P_{-}^{(H)} \otimes ran P_{-}^{(V)})$ ;

(e) vector identities: for all $u, v \in H$ and $χ, χ^{'} \in V$ , $Θ (P_{-}^{(H \otimes V)} ((u \otimes χ) \otimes (v \otimes χ^{'}))) = P_{+}^{(H)} (u \otimes v) \otimes P_{-}^{(V)} (χ \otimes χ^{'}) + P_{-}^{(H)} (u \otimes v) \otimes P_{+}^{(V)} (χ \otimes χ^{'}),$ $Θ (P_{+}^{(H \otimes V)} ((u \otimes χ) \otimes (v \otimes χ^{'}))) = P_{+}^{(H)} (u \otimes v) \otimes P_{+}^{(V)} (χ \otimes χ^{'}) + P_{-}^{(H)} (u \otimes v) \otimes P_{-}^{(V)} (χ \otimes χ^{'});$

(f) dimensions: $\dim ran P_{-}^{(H \otimes V)} = (\binom{m}{2}) (\binom{k + 1}{2}) + (\binom{m + 1}{2}) (\binom{k}{2}) = (\binom{m k}{2}),$ with the two summands of (d) having dimensions $(\binom{m}{2}) (\binom{k + 1}{2})$ and $(\binom{m + 1}{2}) (\binom{k}{2})$ .

Facts & Assumptions

Given: The finite-dimensional nonzero complex Hilbert spaces $H, V$ of dimensions $m, k$ , their completed tensor products, the elementary tensors and the permutation projections and exchange operators of the cited items.

[F1]

Tensor construction. For complex Hilbert spaces $X, Y$ the inclusion $κ : X ⊙ Y \to X \hat{\otimes} Y$ is a linear isometry with dense image; $κ (u \otimes v)$ is bilinear, $∥ κ (u \otimes v) ∥ = ∥ u ∥ ∥ v ∥$ and $⟨ κ (u \otimes v), κ (u^{'} \otimes v^{'}) ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩$ ; every element of $X ⊙ Y$ is a finite sum of elementary tensors, and if $(e_{a})$ and $(f_{b})$ are orthonormal bases of $X$ and $Y$ then $(κ (e_{a} \otimes f_{b}))$ is an orthonormal basis of $X \hat{\otimes} Y$ (Hilbert tensor construction: inner product, completion and product bases clauses (a)-(d)).

[F2]

Multilinear factorisation. For a finite list of modules $M_{1}, \dots, M_{k}$ over a commutative ring, every parenthesised tensor product represents multilinear maps from $M_{1} \times \dots \times M_{k}$ , and different parenthesizations are connected by the unique isomorphism preserving pure tensors (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F3]

Finite-dimensional subspaces are closed. A subspace of a normed space that admits a finite basis is closed (A finite-dimensional normed subspace is closed).

[F4]

Exchange operators and projections. For a Hilbert space $W$ , the exchange operator $τ_{W} : = U_{(0 1)}$ satisfies $τ_{W}^{2} = I$ and $τ_{W}^{*} = τ_{W}$ and $τ_{W} (w \otimes w^{'}) = w^{'} \otimes w$ , and $P_{\pm}^{(W)} = \frac{1}{2} (I \pm τ_{W})$ are the orthogonal projections with the corresponding ranges (The two-particle exchange operator and the symmetric and antisymmetric combinations clauses (a),(b), Permutation sector projections on the n-fold tensor power clauses (a),(c)).

[F5]

Bounded tensor maps. For bounded operators $S, S^{'}$ on $X$ and $T, T^{'}$ on $Y$ there is a unique bounded $S \otimes T$ with $(S \otimes T) κ (u \otimes v) = κ^{'} (S u \otimes T v)$ , $∥ S \otimes T ∥ \leq ∥ S ∥ ∥ T ∥$ , $(S \otimes T) (S^{'} \otimes T^{'}) = (S S^{'}) \otimes (T T^{'})$ , $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ , and unitarity of $S, T$ gives unitarity of $S \otimes T$ (Bounded tensor maps: extension, norm estimate, adjoint and commutation clauses (a)-(d), A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F6]

Dimensions. For finite-dimensional vector spaces $X, Y$ over a field one has $\dim (X \otimes Y) = \dim X \cdot \dim Y$ ( $R^{m} \otimes_{R} R^{n} ≅ R^{m n}$ with the product basis, and $\dim_{F} (V \otimes_{F} W) = \dim_{F} V \dim_{F} W$ ); and $\dim ran P_{-}^{(n)} = (\binom{d}{n})$ , $\dim ran P_{+}^{(n)} = (\binom{n + d - 1}{n})$ for a $d$ -dimensional space (Slater and symmetric occupation-number bases of the finite-dimensional permutation sectors clauses (b),(c)).

[F7]

Orthogonal projections. If $P, Q$ are orthogonal projections with $P Q = Q P = 0$ , then $P + Q$ is an orthogonal projection with $ran (P + Q) = ran P + ran Q$ a direct sum of orthogonal subspaces; a product $P \otimes Q$ of orthogonal projections is an orthogonal projection (The Hilbert orthogonal projection onto a closed subspace, Permutation sector projections on the n-fold tensor power clause (b)).

Proof

technique · direct; identify the finite-dimensional algebraic and completed tensor products, build the regrouping map from the multilinear factorisation of the four-variable assignment, verify inversion and isometry on elementary tensors, transfer the exchange and symmetriser identities from elementary tensors by linearity, and read the decompositions and dimensions off the resulting projection identities

Given: The data of the statement and [F1]-[F7].

1.1F1F3algebra

[Identification] By [F1] the inclusion $κ : H ⊙ V \to H \hat{\otimes} V$ is a linear isometry with dense image; if $(e_{1}, \dots, e_{m})$ and $(f_{1}, \dots, f_{k})$ are orthonormal bases of $H$ and $V$ , then the $m k$ elements $e_{a} \otimes f_{b}$ span the algebraic tensor product by bilinearity, so $κ [H ⊙ V]$ is a finite-dimensional subspace of the Hilbert space $H \hat{\otimes} V$ , hence closed by [F3], and a dense closed subspace is the whole space; thus $κ$ is onto and identifies the two spaces, and the same argument applies to the algebraic and completed tensor products of $H \otimes V$ with itself and of $H \otimes H$ with $V \otimes V$ , whose algebraic parts are spanned by finitely many elementary tensors. This proves (a).

2.1F1F2step 1.1algebraconstruct

[The regrouping map and its inverse] Define $Φ (u, v, χ, χ^{'}) : = (u \otimes v) \otimes (χ \otimes χ^{'})$ for $u, v \in H$ , $χ, χ^{'} \in V$ ; it is multilinear in its four arguments, so by [F2] it corresponds to a unique linear map on the four-fold algebraic tensor product and, by the parenthesization independence of [F2] together with the identification of step 1.1, to a unique linear map $Θ$ on $(H \otimes V) \hat{\otimes} (H \otimes V)$ with the displayed values on elementary tensors; uniqueness holds because those elementary tensors span the space. Likewise $Ψ ((u \otimes v) \otimes (χ \otimes χ^{'})) : = (u \otimes χ) \otimes (v \otimes χ^{'})$ is multilinear and defines a linear map $Ψ$ on $(H \otimes H) \hat{\otimes} (V \otimes V)$ . On elementary tensors $Ψ Θ = i d$ and $Θ Ψ = i d$ , and two linear maps agreeing on a spanning set agree everywhere; hence $Θ$ is a linear isomorphism with inverse $Ψ$ , which is the existence and inverse statement of (b).

3.1F1step 2.1algebra

[Unitarity] For elementary tensors $x = (u \otimes χ) \otimes (v \otimes χ^{'})$ and $y = (u^{'} \otimes χ^{''}) \otimes (v^{'} \otimes χ^{'''})$ in the domain the inner-product identities of [F1] give $⟨ Θ x, Θ y ⟩ = ⟨ u \otimes v, u^{'} \otimes v^{'} ⟩ ⟨ χ \otimes χ^{'}, χ^{''} \otimes χ^{'''} ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩ ⟨ χ, χ^{''} ⟩ ⟨ χ^{'}, χ^{'''} ⟩ = ⟨ x, y ⟩$ ; the difference of the two sesquilinear forms vanishes on all pairs of elementary tensors, and since every vector is a finite sum of elementary tensors by [F1] it vanishes identically, so $Θ$ is an isometry; being invertible by step 2.1 it is unitary, which completes (b).

3.2F4F5step 2.1algebra

[Intertwining with the exchange operators] For $u, v \in H$ , $χ, χ^{'} \in V$ one computes with [F4] and [F5] that $Θ τ_{H \otimes V} ((u \otimes χ) \otimes (v \otimes χ^{'})) = Θ ((v \otimes χ^{'}) \otimes (u \otimes χ)) = (v \otimes u) \otimes (χ^{'} \otimes χ)$ and $(τ_{H} \otimes τ_{V}) Θ ((u \otimes χ) \otimes (v \otimes χ^{'})) = (τ_{H} \otimes τ_{V}) ((u \otimes v) \otimes (χ \otimes χ^{'})) = (v \otimes u) \otimes (χ^{'} \otimes χ)$ ; both sides are bounded linear maps agreeing on the spanning set of elementary tensors, so they agree everywhere, which is (c).

4.1F4F5step 3.2algebra

[Symmetriser identities] By [F4], $P_{\pm}^{(H \otimes V)} = \frac{1}{2} (I \pm τ_{H \otimes V})$ , $P_{\pm}^{(H)} = \frac{1}{2} (I \pm τ_{H})$ and $P_{\pm}^{(V)} = \frac{1}{2} (I \pm τ_{V})$ ; using step 3.2 to move $Θ$ past $τ_{H \otimes V}$ and the linearity and multiplicativity of the tensor product of operators [F5], one obtains on the whole space $Θ P_{-}^{(H \otimes V)} = \frac{1}{2} Θ - \frac{1}{2} (τ_{H} \otimes τ_{V}) Θ = (\frac{1}{2} - \frac{1}{2} τ_{H} \otimes τ_{V}) Θ = (P_{-}^{(H)} \otimes P_{+}^{(V)} + P_{+}^{(H)} \otimes P_{-}^{(V)}) Θ$ , because $\frac{1}{2} (I - τ_{H} \otimes τ_{V}) = \frac{1}{2} (I - τ_{H}) \otimes \frac{1}{2} (I + τ_{V}) + \frac{1}{2} (I + τ_{H}) \otimes \frac{1}{2} (I - τ_{V})$ and its sign-reversed analogue are identities of bounded operators; this proves the first assertion of (d), and the computation with both signs reversed gives the second.

5.1F7step 3.1step 4.1algebra

[Direct-sum decompositions] By [F7] the operators $P_{-}^{(H)} \otimes P_{+}^{(V)}$ and $P_{+}^{(H)} \otimes P_{-}^{(V)}$ are orthogonal projections whose product is $(P_{-}^{(H)} P_{+}^{(H)}) \otimes (P_{+}^{(V)} P_{-}^{(V)}) = 0$ , so their sum is an orthogonal projection with range the orthogonal direct sum of the two ranges; by step 4.1 and the unitarity of step 3.1, the image of $ran P_{-}^{(H \otimes V)}$ under $Θ$ is that direct sum, and the same argument with the second identity of step 4.1 gives the symmetric-sector decomposition, completing (d).

5.2step 4.1algebra

[Vector identities] Applying the first identity of step 4.1 to the elementary tensor $(u \otimes χ) \otimes (v \otimes χ^{'})$ and using the linearity of $Θ$ and of tensor products of operators gives $Θ P_{-}^{(H \otimes V)} ((u \otimes χ) \otimes (v \otimes χ^{'})) = (P_{-}^{(H)} \otimes P_{+}^{(V)} + P_{+}^{(H)} \otimes P_{-}^{(V)}) ((u \otimes v) \otimes (χ \otimes χ^{'})) = P_{+}^{(H)} (u \otimes v) \otimes P_{-}^{(V)} (χ \otimes χ^{'}) + P_{-}^{(H)} (u \otimes v) \otimes P_{+}^{(V)} (χ \otimes χ^{'})$ , which is the first identity of (e); the second follows in the same way from the second identity of step 4.1.

6.1F6step 3.1step 5.1algebra

[Dimensions] By step 5.1 and the unitarity of step 3.1, $\dim ran P_{-}^{(H \otimes V)} = \dim (ran P_{-}^{(H)} \otimes ran P_{+}^{(V)}) + \dim (ran P_{+}^{(H)} \otimes ran P_{-}^{(V)})$ ; by [F6] applied to the $m$ - and $k$ -dimensional spaces this is $(\binom{m}{2}) (\binom{k + 1}{2}) + (\binom{m + 1}{2}) (\binom{k}{2})$ , which are the displayed summand dimensions, and expanding the two products gives $\frac{m (m - 1) k (k + 1) + m (m + 1) k (k - 1)}{4} = \frac{m k (m k - 1)}{2} = (\binom{m k}{2})$ , which is (f).

7.1step 1.1step 2.1step 3.1step 3.2step 4.1step 5.1step 5.2step 6.1∎

[Assembly] Step 1.1 proves (a), steps 2.1 and 3.1 prove (b), step 3.2 proves (c), steps 4.1 and 5.1 prove (d), step 5.2 proves (e) and step 6.1 proves (f). Only the cited linear algebra, tensor products and permutation projections were used, under the Countable Choice hypotheses of [F1], [F2] and [F5]; no physical reading of the factors is asserted.

Remarks

Reading of the decomposition. With $H$ an orbital factor and $V$ an internal (spin) factor, the first summand of the antisymmetric sector pairs antisymmetric orbital two-vectors with symmetric internal two-vectors and the second pairs symmetric orbital two-vectors with antisymmetric internal two-vectors, so the internal permutation symmetry is opposite to the orbital one. The physical use of this identity for two spin-half fermions is developed on the identical-particles examples page.
Finite dimension. Both factors are finite dimensional, so the algebraic and completed tensor products are identified in (a); no infinite-dimensional regrouping is asserted, and the identities themselves are transferred from elementary tensors by linearity.

Regrouping two factors: the symmetry decomposition of a two-particle sector over an orbital and an internal factor

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources