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_reducible]
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) :
@[instance_reducible]
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 := ⋯ }
@[instance_reducible]
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] :