Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated
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 (ACω)). Let H,K 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 H as a right C-module by u⋅c:=cu and K as a left C-module by c⋅v:=cv. Write H⊙K for the complex vector space of The tensor product M⊗RN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums applied to these modules: its underlying abelian group is the quotient F/H0 of that definition, the class of e(u,v) is written u⊗v, every element of H⊙K is a finite sum of elementary tensors u⊗v, and the defining relations make (u,v)↦u⊗v C-bilinear. Define, for finite sums,

⟨∑iui⊗vi, ∑juj′⊗vj′⟩:=∑i,j⟨ui,uj′⟩H ⟨vi,vj′⟩K.

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 H⊙K, linear in the first argument and conjugate-linear in the second;

(b) positive definiteness and orthonormal coordinates: ⟨z,z⟩≥0 for every z∈H⊙K, with ⟨z,z⟩=0 exactly for z=0; more precisely, if U0⊆H and V0⊆K are finite-dimensional subspaces with orthonormal bases e1,…,ep and f1,…,fq, then every z in the span of the elementary tensors from U0×V0 has a unique expansion z=∑a,bcab ea⊗fb and ⟨z,z⟩=∑a,b∣cab∣2; in particular the assignment is an inner product on H⊙K;

(c) completion: the norm completion (H⊙K^,κ) of H⊙K (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, ∥κ(u⊗v)∥=∥u∥ ∥v∥, and any two completions of H⊙K are identified by a unique surjective linear isometry fixing H⊙K pointwise;

(d) product bases: if (ea)a∈A and (fb)b∈B are orthonormal families in H and K whose closed linear spans are H and K, then (κ(ea⊗fb))(a,b)∈A×B is an orthonormal family in H⊙K^ whose closed linear span is H⊙K^; if A and B are countable then H⊙K^ is separable.

The notation H⊗^K:=H⊙K^ is used in the rest of this pair. More precisely, if (Y,ι) and (Z,j) are any two norm completions of H⊙K, there is a unique surjective linear isometry U:Y→Z with U∘ι=j. No assertion is made about unbounded operators or algebraic sums of non-completed tensor products.

Facts & Assumptions

Given: Complex Hilbert spaces H,K with pairing linear in the first argument; the algebraic tensor product H⊙K of The tensor product M⊗RN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums over R=C; the displayed sesquilinear form; finite sums of elementary tensors.

[F1]

The tensor product M⊗RN is the quotient of the free Z-module F=Z(M×N) by the subgroup generated by e(m+m′,n)−e(m,n)−e(m′,n), e(m,n+n′)−e(m,n)−e(m,n′) and e(mr,n)−e(m,rn); its elements are the cosets m⊗n, every tensor is a finite sum of elementary tensors, the relations (m+m′)⊗n=m⊗n+m′⊗n, m⊗(n+n′)=m⊗n+m⊗n′ and (mr)⊗n=m⊗(rn) hold, and 0⊗n=0=m⊗0 (The tensor product M⊗RN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums).

[F2]

A completion of a normed space X is a pair (X^,ι) with X^ Banach, ι:X→X^ a linear isometry and ι[X] dense; and if X 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).

[F3]

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 ∥v∥=⟨v,v⟩1/2 (Real and complex inner-product spaces and their induced length, The induced length is a norm).

[F4]

Every finite-dimensional complex inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).

[F5]

For an orthonormal family (gi)i∈I in a Hilbert space the finite partial sums PFx=∑i∈F⟨x,gi⟩gi converge to x for every x 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).

[F6]

In a complex inner product space, ∣⟨x,y⟩∣≤∥x∥ ∥y∥, and ∥x∥=0 implies x=0 (Cauchy–Schwarz: ∣⟨u,v⟩∣≤∥u∥∥v∥, with equality exactly for linearly dependent vectors, Orthogonality and the orthogonal complement).

Proof

technique · direct: descend the coordinate functionals through the defining relations, verify the sesquilinear form and its positive definiteness in orthonormal coordinates of the finite-dimensional factor spans, complete, and extend the product-basis density by the norm estimate for elementary products
1.1givenF1algebra

[The quotient is a complex vector space] Since C is commutative, for each c∈C the Z-linear self-map Lc of F induced by e(u,v)↦e(cu,v) maps every defining generator of H0 to a defining generator: Lc(e(u+u′,v)−e(u,v)−e(u′,v))=e(cu+cu′,v)−e(cu,v)−e(cu′,v) is the first relation at (cu,cu′,v), the second family is preserved in the same way, and Lc(e(ur,v)−e(u,rv))=e(c(ur),v)−e(cu,rv) is the third relation at (cu,r,v) because c(ur)=(cu)r. Hence Lc[H0]⊆H0 and Lc descends to a Z-linear map of F/H0; because LcLc′=Lcc′ and the actions distribute over the abelian group, F/H0 becomes a C-vector space with c⋅(u⊗v)=(cu)⊗v; the third relation gives (cu)⊗v=u⊗(cv), so the quotient is the C-bilinear tensor product H⊙K.

2.1givenF1F3step 1.1algebra

[Well-definedness and sesquilinearity] For fixed (u0,v0), put bu0,v0(u,v)=⟨u,u0⟩H⟨v,v0⟩K. By [F3] this is C-bilinear in u,v, and bu0,v0(ur,v)=rbu0,v0(u,v)=bu0,v0(u,rv). Extend its values on the basis of F=Z(H×K) by b~u0,v0(∑inie(ui,vi))=∑inibu0,v0(ui,vi) for ni∈Z. This is a Z-linear map on F, and additivity in each variable and the displayed balancing identity show that it vanishes on all three families of generators of H0 in [F1], hence on H0. It therefore induces an additive functional λu0,v0:F/H0→C. Since b~u0,v0(Lcx)=cb~u0,v0(x) for every x∈F, the scalar action of step 1.1 makes λu0,v0 complex-linear. For any finite representation w=∑juj′⊗vj′, the displayed form is consequently independent of the representation of its first argument z, being ∑jλuj′,vj′(z). On free representatives, conjugate symmetry of the factor pairings gives ⟨z,w⟩=⟨w,z⟩‾ term by term. Independence in the first argument applied to the right-hand side therefore gives independence of the representation of w as well. The descended form is linear in z; conjugate symmetry then makes it conjugate-linear in w, and proves it is Hermitian.

3.1step 1.1step 2.1F4F6algebra

[Positive definiteness and unique orthonormal coordinates] Let z=∑i=1nui⊗vi, let U0=span⁡{ui} and V0=span⁡{vi}, and choose orthonormal bases e1,…,ep of U0 and f1,…,fq of V0 by [F4]. Write ui=∑aαiaea and vi=∑bβibfb; bilinearity of ⊗ (step 1.1) gives z=∑a,bcabea⊗fb with cab=∑iαiaβib. By the defining formula of the Statement and orthonormality, ⟨z,z⟩=∑a,b,c,dcabccd‾⟨ea,ec⟩⟨fb,fd⟩=∑a,b∣cab∣2≥0. If z=0, then this same displayed formula gives ∑a,b∣cab∣2=⟨z,z⟩=0, so every cab=0, because a sum of nonnegative real numbers vanishes only if every term does; conversely, if cab=0 for all a,b then bilinearity gives z=∑a,b0⋅ea⊗fb=0. Hence ⟨z,z⟩=0 exactly when z=0, and applying the same argument to the difference of two expansions shows that the coefficients relative to orthonormal families are unique.

4.1step 3.1F2F3constructalgebra

[Completion and the norm of elementary tensors] By steps 2.1 and 3.1, (H⊙K,⟨⋅,⋅⟩) is a complex inner product space with induced norm ∥z∥=⟨z,z⟩1/2 by [F3]. Its norm completion (H⊙K^,κ) 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 H⊙K^ is a Hilbert space and κ is a linear isometry with dense image. The norm of an elementary tensor is ∥κ(u⊗v)∥2=⟨u⊗v,u⊗v⟩=⟨u,u⟩H⟨v,v⟩K=∥u∥2∥v∥2, hence ∥κ(u⊗v)∥=∥u∥ ∥v∥. To prove the completion uniqueness asserted above, let (Y,ι) and (Z,j) be completions. The rule ι(z)↦j(z) is a well-defined linear isometry on the dense subspace ι[H⊙K]. For y∈Y, choose zn∈H⊙K with ι(zn)→y and define U(y):=lim⁡nj(zn); the isometry makes (j(zn)) Cauchy and makes this limit independent of the approximating sequence. Thus U is a linear isometry with U∘ι=j. Its image is closed because Y is complete and contains the dense set j[H⊙K], so it is onto; any two such continuous extensions agree on a dense subspace and hence everywhere.

5.1step 4.1F1algebra

[Orthonormal family of products] Let (ea)a∈A, (fb)b∈B be orthonormal with closed linear spans H and K. For pairs (a,b)≠(a′,b′) at least one index differs, so ⟨κ(ea⊗fb),κ(ea′⊗fb′)⟩=⟨ea,ea′⟩H⟨fb,fb′⟩K=0, and for equal pairs the value is 1; hence the products are orthonormal in H⊙K^.

6.1step 4.1step 5.1F5F6algebra∎

[Density of the product span] Fix ε>0 and z=∑i=1nui⊗vi∈H⊙K. By [F5] applied to (ea) and to (fb) there are finite sets Ai⊆A, Bi⊆B with ∥ui−∑a∈Ai⟨ui,ea⟩ea∥<ε/(n(∥vi∥+1)) and ∥vi−∑b∈Bi⟨vi,fb⟩fb∥<ε/(n(∥ui∥+1)); write ui′,vi′ for the finite sums and z′=∑iui′⊗vi′. Then z−z′=∑i((ui−ui′)⊗vi+ui′⊗(vi−vi′)), and by the triangle inequality, ∥ui′∥≤∥ui∥ (Bessel, [F5]) and the norm formula of step 4.1, ∥z−z′∥≤∑i(∥ui−ui′∥ ∥vi∥+∥ui∥ ∥vi−vi′∥)<2ε. Hence every element of the dense subspace κ[H⊙K] is approximated by finite sums ∑cabκ(ea⊗fb), so the closed linear span of the product family contains κ[H⊙K] and therefore coincides with H⊙K^; by [F5] the family is a complete orthonormal system. If A and B are countable, then A×B is countable and the closed span of a countable family is separable, so H⊙K^ is separable.

Depends on

Used by

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