feat(Algebra/Star/LinearMap): star mul' = mul' ∘ TensorProduct.comm and star (f ⊗ₘ g) = star f ⊗ₘ star g (#31003)

Author: themathqueen

Mathlib/Algebra/Star/LinearMap.lean

@@ -5,6 +5,7 @@ Authors: Monica Omar
 -/
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Star.SelfAdjoint
+import Mathlib.Algebra.Star.TensorProduct
 
 /-!
 # Intrinsic star operation on `E →ₗ[R] F`
@@ -52,10 +53,12 @@ def intrinsicStarAddMonoid : StarAddMonoid (E →ₗ[R] F) where
 
 scoped[IntrinsicStar] attribute [instance] LinearMap.intrinsicStarAddMonoid
 
+/-- A linear map is self-adjoint (with respect to the intrinsic star) iff it is star-preserving. -/
 theorem isSelfAdjoint_iff_map_star (f : E →ₗ[R] F) :
     IsSelfAdjoint f ↔ ∀ x, f (star x) = star (f x) := by
   simp_rw [IsSelfAdjoint, LinearMap.ext_iff, intrinsicStar_apply, star_eq_iff_star_eq, eq_comm]
 
+/-- A star-preserving linear map is self-adjoint (with respect to the intrinsic star). -/
 @[simp]
 protected theorem _root_.StarHomClass.isSelfAdjoint {S : Type*} [FunLike S E F]
     [LinearMapClass S R E F] [StarHomClass S E F] {f : S} : IsSelfAdjoint (f : E →ₗ[R] F) :=
@@ -71,25 +74,44 @@ theorem intrinsicStar_comp (f : E →ₗ[R] F) (g : G →ₗ[R] E) :
 @[simp] theorem intrinsicStar_zero : star (0 : E →ₗ[R] F) = 0 := by ext; simp
 
 section NonUnitalNonAssocSemiring
-variable {E : Type*} [NonUnitalNonAssocSemiring E] [StarRing E] [Module R E]
-  [StarModule R E] [SMulCommClass R E E] [IsScalarTower R E E]
+variable {R' E : Type*} [CommSemiring R'] [StarRing R']
+  [NonUnitalNonAssocSemiring E] [StarRing E] [Module R E] [Module R' E]
+  [StarModule R E] [StarModule R' E] [SMulCommClass R E E] [IsScalarTower R E E]
 
 theorem intrinsicStar_mulLeft (x : E) : star (mulLeft R x) = mulRight R (star x) := by ext; simp
 
 theorem intrinsicStar_mulRight (x : E) : star (mulRight R x) = mulLeft R (star x) := by
   rw [star_eq_iff_star_eq, intrinsicStar_mulLeft, star_star]
 
--- TODO: when we have `Star (E ⊗[R] F)` (PR #27290), we can do these two:
--- `star (mul' R E) = mul' R E ∘ₗ TensorProduct.comm R E E`
--- `star (f ⊗ₘ g) = star f ⊗ₘ star g`
+theorem intrinsicStar_mul' [SMulCommClass R' E E] [IsScalarTower R' E E] :
+    star (mul' R' E) = mul' R' E ∘ₗ TensorProduct.comm R' E E :=
+  TensorProduct.ext' fun _ _ ↦ by simp
 
 end NonUnitalNonAssocSemiring
 
-variable [SMulCommClass R R F]
-
+variable [SMulCommClass R R F] in
 lemma intrinsicStarModule : StarModule R (E →ₗ[R] F) where
   star_smul _ _ := by ext; simp
 
 scoped[IntrinsicStar] attribute [instance] LinearMap.intrinsicStarModule
 
+section TensorProduct
+variable {R E F G H : Type*} [CommSemiring R] [StarRing R]
+  [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E]
+  [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F]
+  [AddCommMonoid G] [StarAddMonoid G] [Module R G] [StarModule R G]
+  [AddCommMonoid H] [StarAddMonoid H] [Module R H] [StarModule R H]
+
+theorem _root_.TensorProduct.intrinsicStar_map (f : E →ₗ[R] F) (g : G →ₗ[R] H) :
+    star (TensorProduct.map f g) = TensorProduct.map (star f) (star g) :=
+  TensorProduct.ext' fun _ _ ↦ by simp
+
+theorem intrinsicStar_lTensor (f : F →ₗ[R] G) : star (lTensor E f) = lTensor E (star f) := by
+  simp [lTensor, TensorProduct.intrinsicStar_map]
+
+theorem intrinsicStar_rTensor (f : E →ₗ[R] F) : star (rTensor G f) = rTensor G (star f) := by
+  simp [rTensor, TensorProduct.intrinsicStar_map]
+
+end TensorProduct
+
 end LinearMap

Mathlib/Algebra/Star/TensorProduct.lean

@@ -7,10 +7,10 @@ import Mathlib.Algebra.Star.Module
 import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 /-!
+# 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.
-
 -/
 
 namespace TensorProduct
@@ -22,20 +22,24 @@ variable {R A B : Type*}
 open scoped TensorProduct
 
 instance : Star (A ⊗[R] B) where
-  star x := map (starLinearEquiv R (A := A)) (starLinearEquiv R).toLinearMap x
+  star x := congr (starLinearEquiv R) (starLinearEquiv R) x
 
 @[simp]
 theorem star_tmul (x : A) (y : B) : star (x ⊗ₜ[R] y) = star x ⊗ₜ[R] star y := rfl
 
 noncomputable instance : InvolutiveStar (A ⊗[R] B) where
   star_involutive x := by
-    simp only [star, map_map, LinearEquiv.comp_coe]
-    convert congr($map_id x) <;> ext <;> simp
+    simp_rw [star]
+    rw [congr_congr]
+    convert congr($congr_refl_refl x) <;> ext <;> simp
 
 noncomputable instance : StarAddMonoid (A ⊗[R] B) where
   star_add := LinearMap.map_add _
 
 instance : StarModule R (A ⊗[R] B) where
   star_smul := LinearMap.map_smulₛₗ _
 
+theorem _root_.starLinearEquiv_tensor :
+    starLinearEquiv R (A := A ⊗[R] B) = congr (starLinearEquiv R) (starLinearEquiv R) := rfl
+
 end TensorProduct

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -973,13 +973,21 @@ theorem congr_symm (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N
 @[simp] theorem congr_refl_refl : congr (.refl R M) (.refl R N) = .refl R _ :=
   LinearEquiv.toLinearMap_injective <| ext' fun _ _ ↦ rfl
 
-theorem congr_trans {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃]
-    {σ₃₁ : R₃ →+* R} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃]
-    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
-    (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂) (g₁ : N ≃ₛₗ[σ₁₂] N₂) :
-    congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) :=
+section congr_congr
+variable {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃]
+  {σ₃₁ : R₃ →+* R} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃]
+  [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
+  (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂) (g₁ : N ≃ₛₗ[σ₁₂] N₂)
+
+theorem congr_trans : congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) :=
   LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _
 
+theorem congr_congr (x : M ⊗[R] N) :
+    congr f₂ g₂ (congr f₁ g₁ x) = congr (f₁.trans f₂) (g₁.trans g₂) x :=
+  DFunLike.congr_fun (congr_trans ..).symm x
+
+end congr_congr
+
 theorem congr_mul (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N) :
     congr (f * f') (g * g') = congr f g * congr f' g' := congr_trans _ _ _ _