Imports
/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module
public import Mathlib.Analysis.InnerProductSpace.Completion
public import Mathlib.Analysis.InnerProductSpace.TensorProduct
public import Mathlib.Analysis.Normed.Operator.Extend
public import Physlib.Meta.TODO.BasicComplete tensor product
i. Overview
Given two inner product spaces E and F over 𝕜, their tensor product E ⊗[𝕜] F consists
of finite sums of simple (a.k.a. pure) tensors m ⊗ₜ[𝕜] n. This tensor product is again an inner
product space with inner product defined by ⟪m ⊗ₜ n, m' ⊗ₜ n'⟫_𝕜 = ⟪m, m'⟫_𝕜 * ⟪n, n'⟫_𝕜
on simple tensors and then extended by linearity (c.f. TensorProduct.instInnerProductSpace).
However, in general this procedure does not result in a Hilbert space: Cauchy sequences need not converge because the tensor product does not contain any infinite sums of simple tensors. In order to obtain a Hilbert space for use in quantum mechanics, we must add in the limits of Cauchy sequences by taking the completion.
In this module we define the complete tensor product,
CompleteTensorProduct 𝕜 E F := Completion (E ⊗[𝕜] F) with notation E ⊗ₕ[𝕜] F and E ⊗ₕ F,
provide some basic properties for the maps which embed E ⊗[𝕜] F into E ⊗ₕ[𝕜] F
and prove that ⊗ₕ is commutative and associative (up to linear isometric equivalence).
ii. Key results
CompleteTensorProduct 𝕜 E F (notation E ⊗ₕ[𝕜] F and E ⊗ₕ F) :
The completion of the tensor product of a pair of inner product spaces E and F over 𝕜.
CompleteTensorProduct.comm 𝕜 E F : The linear isometric equivalence between
E ⊗ₕ[𝕜] F and F ⊗ₕ[𝕜] E.
CompleteTensorProduct.assoc 𝕜 E F G : The linear isometric equivalence between
E ⊗ₕ[𝕜] F ⊗ₕ[𝕜] G and E ⊗ₕ[𝕜] (F ⊗ₕ[𝕜] G).
iii. Table of contents
A. Definition
B. Nontrivial
C. Coercions
D. Induction principle
E. Commutative
F. Associative
iv. References
@[expose] public sectionA. Definition
The completion of the tensor product of two inner product spaces E and F over 𝕜.
By construction this produces a Hilbert space. The localized notations are E ⊗ₕ F
and E ⊗ₕ[𝕜] F, accessed by open scoped CompleteTensorProduct.
def CompleteTensorProduct (𝕜 : Type*) [RCLike 𝕜]
(E : Type*) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
(F : Type*) [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : Type _ := Completion (E ⊗[𝕜] F)
deriving NormedAddCommGroup, InnerProductSpace 𝕜, CompleteSpace@[inherit_doc CompleteTensorProduct]
scoped[CompleteTensorProduct] infixl:100 " ⊗ₕ " => CompleteTensorProduct _@[inherit_doc]
scoped[CompleteTensorProduct]
notation:100 E:100 " ⊗ₕ[" 𝕜 "] " F:101 => CompleteTensorProduct 𝕜 E FB. Nontrivial
instance _root_.TensorProduct.instNontrivial : Nontrivial (E ⊗[𝕜] F) where
exists_pair_ne := 𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 Finst✝¹:Nontrivial Einst✝:Nontrivial F⊢ ∃ x y, x ≠ y
𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 Finst✝¹:Nontrivial Einst✝:Nontrivial Fx:Ehx:x ≠ 0⊢ ∃ x y, x ≠ y
𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 Finst✝¹:Nontrivial Einst✝:Nontrivial Fx:Ehx:x ≠ 0y:Fhy:y ≠ 0⊢ ∃ x y, x ≠ y
exact ⟨x ⊗ₜ y, 0, norm_pos_iff.mp (𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 Finst✝¹:Nontrivial Einst✝:Nontrivial Fx:Ehx:x ≠ 0y:Fhy:y ≠ 0⊢ 0 < ‖x ⊗ₜ[𝕜] y‖ All goals completed! 🐙)⟩instance instNontrivial : Nontrivial (E ⊗ₕ[𝕜] F) where
exists_pair_ne := 𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 Finst✝¹:Nontrivial Einst✝:Nontrivial F⊢ ∃ x y, x ≠ y
𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 Finst✝¹:Nontrivial Einst✝:Nontrivial Fx:E ⊗[𝕜] Fhx:x ≠ 0⊢ ∃ x y, x ≠ y
All goals completed! 🐙C. Coercions
The canonical embedding of the tensor product into its completion.
@[coe]
def coe' : E ⊗[𝕜] F → E ⊗ₕ[𝕜] F := Completion.coe'
Coercion from E ⊗[𝕜] F to its completion.
instance : Coe (E ⊗[𝕜] F) (E ⊗ₕ[𝕜] F) := ⟨coe'⟩lemma denseRange_coe : DenseRange (coe' : E ⊗[𝕜] F → E ⊗ₕ[𝕜] F) := Completion.denseRange_coe@[norm_cast]
lemma coe_zero : (0 : E ⊗[𝕜] F) = (0 : E ⊗ₕ[𝕜] F) := rfl@[norm_cast]
lemma coe_neg : (-x : E ⊗[𝕜] F) = (-x : E ⊗ₕ[𝕜] F) := Completion.coe_neg _@[norm_cast]
lemma coe_sub : (x - y : E ⊗[𝕜] F) = (x - y : E ⊗ₕ[𝕜] F) := Completion.coe_sub _ _@[norm_cast]
lemma coe_add : (x + y : E ⊗[𝕜] F) = (x + y : E ⊗ₕ[𝕜] F) := Completion.coe_add _ _@[simp, norm_cast]
lemma coe_smul : (c • x : E ⊗[𝕜] F) = (c • x : E ⊗ₕ[𝕜] F) := Completion.coe_smul _ _@[simp]
lemma inner_coe : ⟪(x : E ⊗ₕ[𝕜] F), (y : E ⊗ₕ[𝕜] F)⟫_𝕜 = ⟪x, y⟫_𝕜 := Completion.inner_coe _ _@[simp]
lemma norm_coe : ‖(x : E ⊗ₕ[𝕜] F)‖ = ‖x‖ := Completion.norm_coe _The canonical embedding of the tensor product into its completion as a linear isometry.
def tInclₗᵢ : E ⊗[𝕜] F →ₗᵢ[𝕜] E ⊗ₕ[𝕜] F := Completion.toComplₗᵢThe canonical embedding of the tensor product into its completion as a continuous linear map.
def tInclL : E ⊗[𝕜] F →L[𝕜] E ⊗ₕ[𝕜] F := tInclₗᵢ.toContinuousLinearMap@[simp]
lemma coe_tInclL : ⇑(tInclL : E ⊗ F →L[𝕜] E ⊗ₕ F) = coe' := rfl@[simp]
lemma norm_tInclL [Nontrivial E] [Nontrivial F] : ‖(tInclL : E ⊗ F →L[𝕜] E ⊗ₕ F)‖ = 1 :=
(tInclₗᵢ : E ⊗ F →ₗᵢ[𝕜] E ⊗ₕ F).norm_toContinuousLinearMapD. Induction principle
An induction principle for CompleteTensorProduct combining those of Completion
and TensorProduct.
@[elab_as_elim]
lemma induction_on {motive : E ⊗ₕ[𝕜] F → Prop} (z : E ⊗ₕ[𝕜] F)
(zero : motive 0) (tmul : ∀ (x : E) (y : F), motive (x ⊗ₜ[𝕜] y))
(add : ∀ x y : E ⊗[𝕜] F, motive x → motive y → motive ↑(x + y))
(closed : IsClosed {x | motive x}) : motive z :=
Completion.induction_on z closed fun x ↦ x.induction_on zero tmul addE. Commutative
The complete tensor product of inner product spaces is commutative, up to linear isometric equivalence.
def comm : E ⊗ₕ[𝕜] F ≃ₗᵢ[𝕜] F ⊗ₕ[𝕜] E :=
(TensorProduct.comm 𝕜 E F).extendOfIsometry tInclₗᵢ.toLinearMap tInclₗᵢ.toLinearMap
denseRange_coe denseRange_coe (𝕜:Type u_1inst✝⁴:RCLike 𝕜E:Type u_2inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_3inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 F⊢ ∀ (x : E ⊗[𝕜] F), ‖tInclₗᵢ.toLinearMap ((TensorProduct.comm 𝕜 E F) x)‖ = ‖tInclₗᵢ.toLinearMap x‖ All goals completed! 🐙)F. Associative
The tensor product of a pair of linear maps with dense range also has dense range.
R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ ‖s - u‖ * ‖v‖ < ε
R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ ‖s - u‖ * ‖v‖ ≤ ‖s - u‖ * (1 + ‖v‖)R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ ‖s - u‖ * (1 + ‖v‖) < ε
R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ ‖s - u‖ * ‖v‖ ≤ ‖s - u‖ * (1 + ‖v‖) exact mul_le_mul_of_nonneg_left (R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ ‖v‖ ≤ 1 + ‖v‖ All goals completed! 🐙) (norm_nonneg _)
R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ ‖s - u‖ * (1 + ‖v‖) < ε exact (lt_div_iff₀ <| R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fv:Fu:Eε:ℝhε:ε > 0s:Ehs:‖s - u‖ < ε / (1 + ‖v‖)⊢ 0 < 1 + ‖v‖ All goals completed! 🐙).mp hs
R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:F⊢ ∀ a ∈ Set.range ⇑f, ∀ b ∈ Set.range ⇑g, a ⊗ₜ[𝕜] b ∈ ↑(TensorProduct.map f g).range.toAddSubmonoid exact fun _ ⟨u, hu⟩ _ ⟨v, hv⟩ ↦ ⟨u ⊗ₜ v, R:Type u_4𝕜:Type u_5inst✝¹⁰:CommSemiring Rinst✝⁹:RCLike 𝕜σ:R →+* 𝕜inst✝⁸:RingHomSurjective σM:Type u_6inst✝⁷:AddCommMonoid Minst✝⁶:Module R MN:Type u_7inst✝⁵:AddCommMonoid Ninst✝⁴:Module R NE:Type u_8inst✝³:NormedAddCommGroup Einst✝²:InnerProductSpace 𝕜 EF:Type u_9inst✝¹:NormedAddCommGroup Finst✝:InnerProductSpace 𝕜 Ff:M →ₛₗ[σ] Ehf:DenseRange ⇑fg:N →ₛₗ[σ] Fhg:DenseRange ⇑gx:E ⊗[𝕜] Fa:Eb:Fx✝³:Ex✝²:x✝³ ∈ Set.range ⇑fx✝¹:Fx✝:x✝¹ ∈ Set.range ⇑gu:Mhu:f u = x✝³v:Nhv:g v = x✝¹⊢ (TensorProduct.map f g) (u ⊗ₜ[R] v) = x✝³ ⊗ₜ[𝕜] x✝¹ All goals completed! 🐙⟩The compete tensor product of inner product spaces is associative, up to linear isometric equivalence.
𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 FG:Type u_4inst✝¹:NormedAddCommGroup Ginst✝:InnerProductSpace 𝕜 G⊢ DenseRange (⇑tInclₗᵢ ∘ ⇑(LinearIsometry.lTensor E tInclₗᵢ))
𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 FG:Type u_4inst✝¹:NormedAddCommGroup Ginst✝:InnerProductSpace 𝕜 G⊢ DenseRange ⇑(LinearIsometry.lTensor E tInclₗᵢ)
All goals completed! 🐙)
fun _ ↦ 𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:InnerProductSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:InnerProductSpace 𝕜 FG:Type u_4inst✝¹:NormedAddCommGroup Ginst✝:InnerProductSpace 𝕜 Gx✝:E ⊗[𝕜] F ⊗[𝕜] G⊢ ‖(tInclₗᵢ.comp (LinearIsometry.lTensor E tInclₗᵢ)).toLinearMap ((TensorProduct.assoc 𝕜 E F G) x✝)‖ =
‖(tInclₗᵢ.comp (LinearIsometry.rTensor G tInclₗᵢ)).toLinearMap x✝‖ All goals completed! 🐙TODO "Prove CompleteTensorProduct.assoc acting on elements of the tensor product
reduces to TensorProduct.assoc. It may be worthwhile to extract and name the linear isometries
(tInclₗᵢ.comp (tInclₗᵢ.rTensor G) : E ⊗[𝕜] F ⊗[𝕜] G →ₗᵢ[𝕜] E ⊗ₕ[𝕜] F ⊗ₕ[𝕜] G) and
(tInclₗᵢ.comp (tInclₗᵢ.lTensor E) : E ⊗[𝕜] (F ⊗[𝕜] G) →ₗᵢ[𝕜] E ⊗ₕ[𝕜] (F ⊗ₕ[𝕜] G))
which embed 3-fold tensor products into their completion."TODO "Define LinearPMap.lTensor/rTensor, TensorProduct.mapP (P = 'partial'?) for the tensor product.
See LinearMap/LinearEquiv/ContinuousLinearMap/LinearIsometry/LinearIsometryEquiv.lTensor/rTensor
and TensorProduct.map/congr/mapL/mapIsometry/congrIsometry for the desired pattern. The tensor
product of two LinearPMaps f and g is the canonical LinearPMap with domain f.domain ⊗ g.domain."TODO "Define CompleteTensorProduct.mapLₕ/mapPₕ/etc. (or a different naming scheme) which take pairs
of continuous/partial/etc. maps or congruences and construct the corresponding map/congruence
on complete tensor products (using, for example, ContinuousLinearMap.extend with tInclL).
c.f. TensorProduct.map/congr/mapL/mapIsometry/congrIsometry."