The star structure on tensor products

This file defines the Star structure on tensor products. This also defines the StarAddMonoid and StarModule instances for tensor products.

instance TensorProduct.instStar {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : Star (TensorProduct R A B)

Equations

• TensorProduct.instStar = { star := fun (x : TensorProduct R A B) => (TensorProduct.congr (starLinearEquiv R) (starLinearEquiv R)) x }

@[simp]

theorem TensorProduct.star_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] (x : A) (y : B) : star (x ⊗ₜ[R] y) = star x ⊗ₜ[R] star y

noncomputable instance TensorProduct.instInvolutiveStar {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : InvolutiveStar (TensorProduct R A B)

Equations

• TensorProduct.instInvolutiveStar = { toStar := TensorProduct.instStar, star_involutive := ⋯ }

noncomputable instance TensorProduct.instStarAddMonoid {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : StarAddMonoid (TensorProduct R A B)

Equations

• TensorProduct.instStarAddMonoid = { toInvolutiveStar := TensorProduct.instInvolutiveStar, star_add := ⋯ }

instance TensorProduct.instStarModule {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : StarModule R (TensorProduct R A B)

theorem starLinearEquiv_tensor {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : starLinearEquiv R = TensorProduct.congr (starLinearEquiv R) (starLinearEquiv R)