Tensor products of finite-dimensional star modules

This file defines the star operation on a tensor product of finite-dimensional star modules and proves compatibility lemmas for tensor-product maps.

@[reducible, inline]

noncomputable abbrev 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] [StarModule 𝕜 E] [StarModule 𝕜 F] : _root_.Star (TensorProduct 𝕜 E F)

Compatibility name for the tensor-product star instance now provided by Mathlib.

Equations

• TensorProduct.Star = inferInstance

@[reducible, inline]

noncomputable abbrev 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] [StarModule 𝕜 E] [StarModule 𝕜 F] : _root_.InvolutiveStar (TensorProduct 𝕜 E F)

Compatibility name for the tensor-product involutive-star instance.

Equations

• TensorProduct.InvolutiveStar = inferInstance

@[reducible, inline]

noncomputable abbrev 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] [StarModule 𝕜 E] [StarModule 𝕜 F] : StarAddMonoid (TensorProduct 𝕜 E F)

Compatibility name for the tensor-product star-additive instance.

Equations

• TensorProduct.starAddMonoid = inferInstance

theorem TensorProduct.starModule {𝕜 : 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] [StarModule 𝕜 E] [StarModule 𝕜 F] : StarModule 𝕜 (TensorProduct 𝕜 E F)

Compatibility name for the tensor-product star-module instance.

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] [StarModule 𝕜 E] [StarModule 𝕜 F] (x y : TensorProduct 𝕜 E F) : star (x + y) = star x + star y

Tensor-product star is additive.

theorem 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] [StarModule 𝕜 E] [StarModule 𝕜 F] : Function.Involutive star

Tensor-product star is involutive.

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] [Module.Finite 𝕜 A] [Module.Finite 𝕜 B] [Module.Finite 𝕜 E] [Module.Finite 𝕜 F] (f : E →ₗ[𝕜] F) (g : A →ₗ[𝕜] B) : (map f g).real = 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] : (mul' 𝕜 A).real = 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] [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] [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] [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] [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] [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] [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] [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

Build a star algebra equivalence from a tensor-product linear equivalence.

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] (f : A ≃⋆ₐ[R] B) (g : C ≃⋆ₐ[R] D) : TensorProduct R A C ≃⋆ₐ[R] TensorProduct R B D

Tensor a pair of star algebra equivalences.

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] (f : A ≃⋆ₐ[R] B) (g : C ≃⋆ₐ[R] D) (x : A) (y : C) : (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] (f : A ≃⋆ₐ[R] B) (g : C ≃⋆ₐ[R] D) (x : B) (y : D) : (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] (f : A ≃⋆ₐ[R] B) : TensorProduct R C A ≃⋆ₐ[R] TensorProduct R C B

Tensor a star algebra equivalence on the left by a fixed algebra.

Equations

• StarAlgEquiv.lTensor C f = StarAlgEquiv.ofAlgEquiv (AlgEquiv.lTensor C f.toAlgEquiv) ⋯

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] (f : A ≃⋆ₐ[R] B) (x : C) (y : A) : (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] (f : A ≃⋆ₐ[R] B) (x : C) (y : B) : (lTensor C f).symm (x ⊗ₜ[R] y) = x ⊗ₜ[R] f.symm y