Tensor Products of Quantum Sets

This file restores the upstream tensor-product quantum-set instance and the fourfold tensor-shuffle lemmas used by later quantum-graph files.

@[implicit_reducible]

noncomputable instance tensorStarAlgebra {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] : starAlgebra (TensorProduct ℂ A B)

Equations

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

theorem modAut_tensor {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] (r : ℝ) : modAut r = AlgEquiv.TensorProduct.map (modAut r) (modAut r)

theorem modAut_tensor_tmul {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] (r : ℝ) (x : A) (y : B) : (modAut r) (x ⊗ₜ[ℂ] y) = (modAut r) x ⊗ₜ[ℂ] (modAut r) y

@[implicit_reducible]

noncomputable instance instInnerProductAlgebraTensorProductComplex {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [InnerProductAlgebra A] [InnerProductAlgebra B] : InnerProductAlgebra (TensorProduct ℂ A B)

Equations

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

@[implicit_reducible]

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.

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

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

theorem comul_real {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] : CoalgebraStruct.comul.real = ↑(TensorProduct.comm ℂ A A) ∘ₗ CoalgebraStruct.comul

noncomputable def swapMiddleTensor (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)

Swap the two middle factors in a fourfold tensor product.

Equations

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

@[simp]

theorem swapMiddleTensor_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) : (swapMiddleTensor R A B C D) (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) = x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w)

@[simp]

theorem swapMiddleTensor_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] : (swapMiddleTensor R A B C D).symm = swapMiddleTensor R A C B D

theorem swapMiddleTensor_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) : ↑(swapMiddleTensor 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) ∘ₗ ↑(swapMiddleTensor R A C E G)

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) ∘ₗ ↑(swapMiddleTensor R A B A B)

theorem swapMiddleTensor_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) : ↑(swapMiddleTensor R B D F H) ∘ₗ TensorProduct.map (TensorProduct.map f g) (TensorProduct.map h k) ∘ₗ ↑(swapMiddleTensor R A C E G).symm = TensorProduct.map (TensorProduct.map f h) (TensorProduct.map g k)

theorem swapMiddleTensor_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 ↑(swapMiddleTensor 𝕜 E F G H) = ↑(swapMiddleTensor 𝕜 E F G H).symm