Monlib.LinearAlgebra.QuantumSet.TensorProduct

source

noncomputable instance tensorStarAlgebra {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [Module.Finite ℂ A] [Module.Finite ℂ B] :

starAlgebra (TensorProduct ℂ A B)

Equations

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

source

theorem modAut_tensor {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [Module.Finite ℂ A] [Module.Finite ℂ B] (r : ℝ) :

modAut r = AlgEquiv.TensorProduct.map (modAut r) (modAut r)

source

theorem modAut_tensor_tmul {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [Module.Finite ℂ A] [Module.Finite ℂ B] (r : ℝ) (x : A) (y : B) :

(modAut r) (x ⊗ₜ[ℂ ] y) = (modAut r) x ⊗ₜ[ℂ ] (modAut r) y

source

noncomputable instance instInnerProductAlgebraTensorProductComplex {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [InnerProductAlgebra A] [InnerProductAlgebra B] [Module.Finite ℂ A] [Module.Finite ℂ B] :

InnerProductAlgebra (TensorProduct ℂ A B)

Equations

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

source

noncomputable instance QuantumSet.tensorProduct {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] [h : Fact (k A = k B)] :

QuantumSet (TensorProduct ℂ A B)

Equations

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

source

theorem QuantumSet.tensorProduct.k_eq₁ {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] [Fact (k A = k B)] :

k (TensorProduct ℂ A B) = k A

source

theorem QuantumSet.tensorProduct.k_eq₂ {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] [h : Fact (k A = k B)] :

k (TensorProduct ℂ A B) = k B

source

theorem comul_real {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] :

CoalgebraStruct.comul.real = ↑(TensorProduct.comm ℂ A A) ∘ₗ CoalgebraStruct.comul

source

noncomputable def swap_middle_tensor (R : Type u_3) [CommSemiring R] (A : Type u_4) (B : Type u_5) (C : Type u_6) (D : Type u_7) [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] :

TensorProduct R (TensorProduct R A B) (TensorProduct R C D) ≃ₗ[R] TensorProduct R (TensorProduct R A C) (TensorProduct R B D)

Equations

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

Instances For

source

@[simp]

theorem swap_middle_tensor_tmul_apply {R : Type u_3} [CommSemiring R] {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A) (y : B) (z : C) (w : D) :

(swap_middle_tensor R A B C D) ((x ⊗ₜ[R] y) ⊗ₜ[R] z ⊗ₜ[R] w) = (x ⊗ₜ[R] z) ⊗ₜ[R] y ⊗ₜ[R] w

source

@[simp]

theorem swap_middle_tensor_symm {R : Type u_3} [CommSemiring R] {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] :

(swap_middle_tensor R A B C D).symm = swap_middle_tensor R A C B D

source

theorem swap_middle_tensor_comp_map {R : Type u_3} [CommSemiring R] {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] [AddCommMonoid E] [AddCommMonoid F] [AddCommMonoid G] [AddCommMonoid H] [Module R E] [Module R F] [Module R G] [Module R H] (f : A →ₗ[R] B) (g : C →ₗ[R] D) (h : E →ₗ[R] F) (k : G →ₗ[R] H) :

↑(swap_middle_tensor R B D F H) ∘ₗ TensorProduct.map (TensorProduct.map f g) (TensorProduct.map h k) = TensorProduct.map (TensorProduct.map f h) (TensorProduct.map g k) ∘ₗ ↑(swap_middle_tensor R A C E G)

source

theorem LinearMap.mul'_tensorProduct {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] :

mul' R (TensorProduct R A B) = TensorProduct.map (mul' R A) (mul' R B) ∘ₗ ↑(swap_middle_tensor R A B A B)

source

theorem swap_middle_tensor_map_conj {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] [AddCommMonoid E] [AddCommMonoid F] [AddCommMonoid G] [AddCommMonoid H] [Module R E] [Module R F] [Module R G] [Module R H] (f : A →ₗ[R] B) (g : C →ₗ[R] D) (h : E →ₗ[R] F) (k : G →ₗ[R] H) :

↑(swap_middle_tensor R B D F H) ∘ₗ TensorProduct.map (TensorProduct.map f g) (TensorProduct.map h k) ∘ₗ ↑(swap_middle_tensor R A C E G).symm = TensorProduct.map (TensorProduct.map f h) (TensorProduct.map g k)

source

theorem swap_middle_tensor_adjoint {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {H : Type u_7} [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] :

LinearMap.adjoint ↑(swap_middle_tensor 𝕜 E F G H) = ↑(swap_middle_tensor 𝕜 E F G H).symm