Tensor product of inner product spaces

This file constructs the tensor product of finite-dimensional inner product spaces.

noncomputable instance TensorProduct.Inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : _root_.Inner 𝕜 (TensorProduct 𝕜 E F)

Equations

• One or more equations did not get rendered due to their size.

theorem TensorProduct.inner_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x z : E) (y w : F) : inner 𝕜 (x ⊗ₜ[𝕜] y) (z ⊗ₜ[𝕜] w) = inner 𝕜 x z * inner 𝕜 y w

theorem TensorProduct.inner_add_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y z : TensorProduct 𝕜 E F) : inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z

theorem TensorProduct.inner_zero_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) : inner 𝕜 x 0 = 0

theorem TensorProduct.inner_conj_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y : TensorProduct 𝕜 E F) : (starRingEnd 𝕜) (inner 𝕜 x y) = inner 𝕜 y x

theorem TensorProduct.inner_zero_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) : inner 𝕜 0 x = 0

theorem TensorProduct.inner_add_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y z : TensorProduct 𝕜 E F) : inner 𝕜 x (y + z) = inner 𝕜 x y + inner 𝕜 x z

theorem TensorProduct.inner_sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n : Type u_4} [Fintype n] (x : n → TensorProduct 𝕜 E F) (y : TensorProduct 𝕜 E F) : inner 𝕜 (∑ i : n, x i) y = ∑ i : n, inner 𝕜 (x i) y

theorem TensorProduct.sum_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n : Type u_4} [Fintype n] (y : TensorProduct 𝕜 E F) (x : n → TensorProduct 𝕜 E F) : inner 𝕜 y (∑ i : n, x i) = ∑ i : n, inner 𝕜 y (x i)

theorem TensorProduct.inner_nonneg_re {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) : 0 ≤ RCLike.re (inner 𝕜 x x)

theorem TensorProduct.eq_span {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) : ∃ (α : ↑(Basis.ofVectorSpaceIndex 𝕜 E) × ↑(Basis.ofVectorSpaceIndex 𝕜 F) → E) (β : ↑(Basis.ofVectorSpaceIndex 𝕜 E) × ↑(Basis.ofVectorSpaceIndex 𝕜 F) → F), ∑ i : ↑(Basis.ofVectorSpaceIndex 𝕜 E) × ↑(Basis.ofVectorSpaceIndex 𝕜 F), α i ⊗ₜ[𝕜] β i = x

@[reducible]

noncomputable instance TensorProduct.normedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : NormedAddCommGroup (TensorProduct 𝕜 E F)

Equations

• TensorProduct.normedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

@[reducible]

noncomputable instance TensorProduct.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : InnerProductSpace 𝕜 (TensorProduct 𝕜 E F)

Equations

• One or more equations did not get rendered due to their size.

theorem TensorProduct.lid_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : LinearMap.adjoint ↑(TensorProduct.lid 𝕜 E) = ↑(TensorProduct.lid 𝕜 E).symm

theorem TensorProduct.comm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : LinearMap.adjoint ↑(TensorProduct.comm 𝕜 E F) = ↑(TensorProduct.comm 𝕜 E F).symm

theorem TensorProduct.assoc_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] : LinearMap.adjoint ↑(TensorProduct.assoc 𝕜 E F G).symm = ↑(TensorProduct.assoc 𝕜 E F G)

theorem TensorProduct.assoc_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] : LinearMap.adjoint ↑(TensorProduct.assoc 𝕜 E F G) = ↑(TensorProduct.assoc 𝕜 E F G).symm

theorem TensorProduct.map_adjoint {𝕜 : Type u_1} [RCLike 𝕜] {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] [FiniteDimensional 𝕜 D] (f : A →ₗ[𝕜] B) (g : C →ₗ[𝕜] D) : LinearMap.adjoint (map f g) = map (LinearMap.adjoint f) (LinearMap.adjoint g)

theorem TensorProduct.inner_ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x z : E) (y w : F) : x ⊗ₜ[𝕜] y = z ⊗ₜ[𝕜] w ↔ ∀ (a : E) (b : F), inner 𝕜 (x ⊗ₜ[𝕜] y) (a ⊗ₜ[𝕜] b) = inner 𝕜 (z ⊗ₜ[𝕜] w) (a ⊗ₜ[𝕜] b)

theorem TensorProduct.forall_inner_eq_zero {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) : (∀ (a : E) (b : F), inner 𝕜 x (a ⊗ₜ[𝕜] b) = 0) ↔ x = 0

theorem TensorProduct.forall_fourfold_inner_eq_zero {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) (TensorProduct 𝕜 G H)) : (∀ (a : E) (b : F) (c : G) (d : H), inner 𝕜 x ((a ⊗ₜ[𝕜] b) ⊗ₜ[𝕜] c ⊗ₜ[𝕜] d) = 0) ↔ x = 0

theorem TensorProduct.inner_ext_iff' {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y : TensorProduct 𝕜 E F) : x = y ↔ ∀ (a : E) (b : F), inner 𝕜 x (a ⊗ₜ[𝕜] b) = inner 𝕜 y (a ⊗ₜ[𝕜] b)

theorem TensorProduct.inner_ext_fourfold_iff' {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) (TensorProduct 𝕜 G H)) : x = y ↔ ∀ (a : E) (b : F) (c : G) (d : H), inner 𝕜 x ((a ⊗ₜ[𝕜] b) ⊗ₜ[𝕜] c ⊗ₜ[𝕜] d) = inner 𝕜 y ((a ⊗ₜ[𝕜] b) ⊗ₜ[𝕜] c ⊗ₜ[𝕜] d)

theorem TensorProduct.lid_symm_adjoint {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : LinearMap.adjoint ↑(TensorProduct.lid 𝕜 E).symm = ↑(TensorProduct.lid 𝕜 E)

theorem TensorProduct.comm_symm_adjoint {𝕜 : Type u_4} {E : Type u_5} {V : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup V] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 V] : LinearMap.adjoint ↑(TensorProduct.comm 𝕜 E V).symm = ↑(TensorProduct.comm 𝕜 E V)