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.
Hilbert tensor construction: inner product, completion and product bases
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let be complex Hilbert spaces with the pairing linear in the first argument (Real and complex inner-product spaces and their induced length, Hilbert space). Regard as a right -module by and as a left -module by . Write for the complex vector space of The tensor product from the additive group underlying the free -module on , elementary tensors, and finite tensor sums applied to these modules: its underlying abelian group is the quotient of that definition, the class of is written , every element of is a finite sum of elementary tensors , and the defining relations make -bilinear. Define, for finite sums,
Then:
(a) well-definedness and sesquilinearity: the displayed value is independent of the representatives of its two arguments and defines a Hermitian sesquilinear form on , linear in the first argument and conjugate-linear in the second;
(b) positive definiteness and orthonormal coordinates: for every , with exactly for ; more precisely, if and are finite-dimensional subspaces with orthonormal bases and , then every in the span of the elementary tensors from has a unique expansion and ; in particular the assignment is an inner product on ;
(c) completion: the norm completion of (Completion of a normed space) exists and, with the unique inner product extending the given one, is a complex Hilbert space; is a linear isometry with dense image, , and any two completions of are identified by a unique surjective linear isometry fixing pointwise;
(d) product bases: if and are orthonormal families in and whose closed linear spans are and , then is an orthonormal family in whose closed linear span is ; if and are countable then is separable.
The notation is used in the rest of this pair. More precisely, if and are any two norm completions of , there is a unique surjective linear isometry with . No assertion is made about unbounded operators or algebraic sums of non-completed tensor products.
Facts & Assumptions
Given: Complex Hilbert spaces with pairing linear in the first argument; the algebraic tensor product of The tensor product from the additive group underlying the free -module on , elementary tensors, and finite tensor sums over ; the displayed sesquilinear form; finite sums of elementary tensors.
The tensor product is the quotient of the free -module by the subgroup generated by , and ; its elements are the cosets , every tensor is a finite sum of elementary tensors, the relations , and hold, and (The tensor product from the additive group underlying the free -module on , elementary tensors, and finite tensor sums).
A completion of a normed space is a pair with Banach, a linear isometry and dense; and if is an inner product space, its norm completion carries a unique inner product extending the given one whose induced length is the completion norm, making it a Hilbert space (Completion of a normed space, The norm completion of an inner-product space is a Hilbert space).
The inner product conventions of the library are: linear in the first argument, conjugate-linear in the second, positive definite, and the induced length is (Real and complex inner-product spaces and their induced length, The induced length is a norm).
Every finite-dimensional complex inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).
For an orthonormal family in a Hilbert space the finite partial sums converge to for every exactly when the closed linear span of the family is the whole space (Orthonormal families, complete orthonormal systems and Hilbert bases, Parseval equivalences for an orthonormal family).
In a complex inner product space, , and implies (Cauchy–Schwarz: , with equality exactly for linearly dependent vectors, Orthogonality and the orthogonal complement).
Proof
[The quotient is a complex vector space] Since is commutative, for each the -linear self-map of induced by maps every defining generator of to a defining generator: is the first relation at , the second family is preserved in the same way, and is the third relation at because . Hence and descends to a -linear map of ; because and the actions distribute over the abelian group, becomes a -vector space with ; the third relation gives , so the quotient is the -bilinear tensor product .
[Well-definedness and sesquilinearity] For fixed , put . By [F3] this is -bilinear in , and . Extend its values on the basis of by for . This is a -linear map on , and additivity in each variable and the displayed balancing identity show that it vanishes on all three families of generators of in [F1], hence on . It therefore induces an additive functional . Since for every , the scalar action of step 1.1 makes complex-linear. For any finite representation , the displayed form is consequently independent of the representation of its first argument , being . On free representatives, conjugate symmetry of the factor pairings gives term by term. Independence in the first argument applied to the right-hand side therefore gives independence of the representation of as well. The descended form is linear in ; conjugate symmetry then makes it conjugate-linear in , and proves it is Hermitian.
[Positive definiteness and unique orthonormal coordinates] Let , let and , and choose orthonormal bases of and of by [F4]. Write and ; bilinearity of (step 1.1) gives with . By the defining formula of the Statement and orthonormality, . If , then this same displayed formula gives , so every , because a sum of nonnegative real numbers vanishes only if every term does; conversely, if for all then bilinearity gives . Hence exactly when , and applying the same argument to the difference of two expansions shows that the coefficients relative to orthonormal families are unique.
[Completion and the norm of elementary tensors] By steps 2.1 and 3.1, is a complex inner product space with induced norm by [F3]. Its norm completion exists by [F2], and by [F2] it carries a unique inner product extending the given one whose induced length is the completion norm; with it is a Hilbert space and is a linear isometry with dense image. The norm of an elementary tensor is , hence . To prove the completion uniqueness asserted above, let and be completions. The rule is a well-defined linear isometry on the dense subspace . For , choose with and define ; the isometry makes Cauchy and makes this limit independent of the approximating sequence. Thus is a linear isometry with . Its image is closed because is complete and contains the dense set , so it is onto; any two such continuous extensions agree on a dense subspace and hence everywhere.
[Orthonormal family of products] Let , be orthonormal with closed linear spans and . For pairs at least one index differs, so , and for equal pairs the value is ; hence the products are orthonormal in .
[Density of the product span] Fix and . By [F5] applied to and to there are finite sets , with and ; write for the finite sums and . Then , and by the triangle inequality, (Bessel, [F5]) and the norm formula of step 4.1, . Hence every element of the dense subspace is approximated by finite sums , so the closed linear span of the product family contains and therefore coincides with ; by [F5] the family is a complete orthonormal system. If and are countable, then is countable and the closed span of a countable family is separable, so is separable.
Depends on
- The tensor product $M\otimes_R N$ from the additive group underlying the free $\mathbb Z$-module on $M\times N$, elementary tensors, and finite tensor sums
- The norm completion of an inner-product space is a Hilbert space
- Completion of a normed space
- Real and complex inner-product spaces and their induced length
- Hilbert space
- Cauchy–Schwarz: $|\langle u,v\rangle|\leq\lVert u\rVert\lVert v\rVert$, with equality exactly for linearly dependent vectors
- Every finite-dimensional real or complex inner product space has an orthonormal basis
- Orthonormal families, complete orthonormal systems and Hilbert bases
- Parseval equivalences for an orthonormal family
- Orthogonality and the orthogonal complement
- The induced length is a norm
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Schwartz/distribution spaces and Hilbert Fock conventions Definition
- Bosonic and fermionic Fock operators with exact domains Lemma
- Bounded tensor maps: extension, norm estimate, adjoint and commutation Lemma
- Fock Creation and Annihilation Operators Satisfy the CAR Lemma
- Permutation sector projections on the n-fold tensor power Lemma
Dependency tree · two levels
55 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
- G. Teschl, Mathematical Methods in Quantum Mechanics, 1st edition 2009, §1.4 pp. 45-47 (tensor construction and product bases) (standard reference, not scraped)
- MIT 8.05 Quantum Physics II (Fall 2013), Chapter 8 'Multiparticle States and Tensor Products', PDF pp. 1-12 (standard reference, not scraped)