tensor_finite

This file defines the star operation on a tensor product of finite-dimensional star-modules $E,F$, i.e., ${(x \otimes y)}^*=x^* \otimes y^*$ for $x\in{E}$ and $x\in{F}$.

noncomputable instance TensorProduct.Star {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : Star (TensorProduct 𝕜 E F)

Equations

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

@[simp]

theorem TensorProduct.star_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [StarModule 𝕜 E] [StarModule 𝕜 F] (x : E) (y : F) : star (x ⊗ₜ[𝕜] y) = star x ⊗ₜ[𝕜] star y

theorem TensorProduct.star_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) (y : TensorProduct 𝕜 E F) : star (x + y) = star x + star y

def TensorProduct.star_is_involutive {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [StarModule 𝕜 E] [StarModule 𝕜 F] : Function.Involutive star

Equations

• ⋯ = ⋯

noncomputable instance TensorProduct.InvolutiveStar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [StarModule 𝕜 E] [StarModule 𝕜 F] : InvolutiveStar (TensorProduct 𝕜 E F)

Equations

• TensorProduct.InvolutiveStar = InvolutiveStar.mk ⋯

noncomputable instance TensorProduct.starAddMonoid {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [StarModule 𝕜 E] [StarModule 𝕜 F] : StarAddMonoid (TensorProduct 𝕜 E F)

Equations

• TensorProduct.starAddMonoid = StarAddMonoid.mk ⋯

instance TensorProduct.starModule {𝕜 : Type u_1} {E : Type u_3} {F : Type u_2} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : StarModule 𝕜 (TensorProduct 𝕜 E F)

Equations

• ⋯ = ⋯

theorem TensorProduct.map_real {𝕜 : Type u_5} [Field 𝕜] [StarRing 𝕜] {A : Type u_1} {B : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup A] [AddCommGroup B] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 A] [Module 𝕜 B] [Module 𝕜 E] [Module 𝕜 F] [StarModule 𝕜 A] [StarModule 𝕜 B] [StarModule 𝕜 E] [StarModule 𝕜 F] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (f : E →ₗ[𝕜] F) (g : A →ₗ[𝕜] B) : (TensorProduct.map f g).real = TensorProduct.map f.real g.real

theorem LinearMap.mul'_real {𝕜 : Type u_2} [Field 𝕜] [StarRing 𝕜] (A : Type u_1) [Ring A] [Module 𝕜 A] [StarRing A] [StarModule 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [FiniteDimensional 𝕜 A] : (LinearMap.mul' 𝕜 A).real = LinearMap.mul' 𝕜 A ∘ₗ ↑(TensorProduct.comm 𝕜 A A)

theorem TensorProduct.assoc_real {𝕜 : Type u_4} {E : Type u_1} {F : Type u_2} {G : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [StarAddMonoid E] [StarAddMonoid F] [StarAddMonoid G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [StarModule 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [StarModule 𝕜 E] [StarModule 𝕜 F] : (↑(TensorProduct.assoc 𝕜 E F G)).real = ↑(TensorProduct.assoc 𝕜 E F G)

theorem TensorProduct.comm_real {𝕜 : Type u_3} {E : Type u_1} {F : Type u_2} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [AddCommGroup F] [StarAddMonoid E] [StarAddMonoid F] [Module 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [StarModule 𝕜 E] [StarModule 𝕜 F] : (↑(TensorProduct.comm 𝕜 E F)).real = ↑(TensorProduct.comm 𝕜 E F)

theorem TensorProduct.lid_real {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [StarAddMonoid E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [StarModule 𝕜 E] : (↑(TensorProduct.lid 𝕜 E)).real = ↑(TensorProduct.lid 𝕜 E)

theorem TensorProduct.rid_real {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [StarAddMonoid E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [StarModule 𝕜 E] : (↑(TensorProduct.rid 𝕜 E)).real = ↑(TensorProduct.rid 𝕜 E)

theorem tensor_op_star_apply {𝕜 : Type u_2} {E : Type u_1} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [StarAddMonoid E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [StarModule 𝕜 E] (x : E) (y : Eᵐᵒᵖ) : star (x ⊗ₜ[𝕜] y) = star x ⊗ₜ[𝕜] (op 𝕜) (star ((unop 𝕜) y))

theorem tenSwap_star {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [StarRing 𝕜] [AddCommGroup E] [StarAddMonoid E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] [StarModule 𝕜 E] (x : TensorProduct 𝕜 E Eᵐᵒᵖ) : star ((tenSwap 𝕜) x) = (tenSwap 𝕜) (star x)

noncomputable def starAlgEquivOfLinearEquivTensorProduct {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [RCLike R] [Ring A] [StarAddMonoid A] [Algebra R A] [StarModule R A] [Ring B] [StarAddMonoid B] [Algebra R B] [StarModule R B] [Semiring C] [Algebra R C] [FiniteDimensional R A] [FiniteDimensional R B] [StarAddMonoid C] (f : TensorProduct R A B ≃ₗ[R] C) (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) (h_one : f (1 ⊗ₜ[R] 1) = 1) (h_star : ∀ (x : A) (y : B), f (star (x ⊗ₜ[R] y)) = star (f (x ⊗ₜ[R] y))) : TensorProduct R A B ≃⋆ₐ[R] C

Equations

• starAlgEquivOfLinearEquivTensorProduct f h_mul h_one h_star = StarAlgEquiv.ofAlgEquiv (Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct f h_mul h_one) ⋯

noncomputable def StarAlgEquiv.TensorProduct.map {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [RCLike R] [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarAddMonoid D] [StarModule R A] [StarModule R B] [StarModule R C] [StarModule R D] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] [Module.Finite R D] (f : A ≃⋆ₐ[R] B) (g : C ≃⋆ₐ[R] D) : TensorProduct R A C ≃⋆ₐ[R] TensorProduct R B D

Equations

• StarAlgEquiv.TensorProduct.map f g = StarAlgEquiv.ofAlgEquiv (AlgEquiv.TensorProduct.map f.toAlgEquiv g.toAlgEquiv) ⋯

theorem StarAlgEquiv.TensorProduct.map_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [RCLike R] [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarAddMonoid D] [StarModule R A] [StarModule R B] [StarModule R C] [StarModule R D] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] [Module.Finite R D] (f : A ≃⋆ₐ[R] B) (g : C ≃⋆ₐ[R] D) (x : A) (y : C) : (StarAlgEquiv.TensorProduct.map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

theorem StarAlgEquiv.TensorProduct.map_symm_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [RCLike R] [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarAddMonoid D] [StarModule R A] [StarModule R B] [StarModule R C] [StarModule R D] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] [Module.Finite R D] (f : A ≃⋆ₐ[R] B) (g : C ≃⋆ₐ[R] D) (x : B) (y : D) : (StarAlgEquiv.TensorProduct.map f g).symm (x ⊗ₜ[R] y) = f.symm x ⊗ₜ[R] g.symm y

noncomputable def StarAlgEquiv.lTensor {R : Type u_1} {A : Type u_2} {B : Type u_3} (C : Type u_4) [RCLike R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarModule R A] [StarModule R B] [StarModule R C] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] (f : A ≃⋆ₐ[R] B) : TensorProduct R C A ≃⋆ₐ[R] TensorProduct R C B

Equations

• StarAlgEquiv.lTensor C f = starAlgEquivOfLinearEquivTensorProduct (LinearEquiv.lTensor C f.toLinearEquiv) ⋯ ⋯ ⋯

theorem StarAlgEquiv.lTensor_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [RCLike R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarModule R A] [StarModule R B] [StarModule R C] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] (f : A ≃⋆ₐ[R] B) (x : C) (y : A) : (StarAlgEquiv.lTensor C f) (x ⊗ₜ[R] y) = x ⊗ₜ[R] f y

theorem StarAlgEquiv.lTensor_symm_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [RCLike R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarModule R A] [StarModule R B] [StarModule R C] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] (f : A ≃⋆ₐ[R] B) (x : C) (y : B) : (StarAlgEquiv.lTensor C f).symm (x ⊗ₜ[R] y) = x ⊗ₜ[R] f.symm y