[Merged by Bors] - feat(LinearAlgebra/BilinearForm/TensorProduct): base change of bilinear forms

Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.BilinearForm
 import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 #align_import linear_algebra.bilinear_form.tensor_product from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
 
@@ -21,52 +22,76 @@ import Mathlib.LinearAlgebra.TensorProduct
 -/
 
 
-universe u v w
+universe u v w uι uR uA uM₁ uM₂
 
-variable {ι : Type*} {R : Type*} {M₁ M₂ : Type*}
+variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂}
 
 open TensorProduct
 
 namespace BilinForm
 
 section CommSemiring
-
-variable [CommSemiring R]
-
+variable [CommSemiring R] [CommSemiring A]
 variable [AddCommMonoid M₁] [AddCommMonoid M₂]
-
-variable [Module R M₁] [Module R M₂]
-
-/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/
-def tensorDistrib : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂) :=
-  ((TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ
-    (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin).toLinearMap ∘ₗ
-  TensorProduct.dualDistrib R _ _ ∘ₗ
-  (TensorProduct.congr (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)
+variable [Algebra R A] [Module R M₁] [Module A M₁]
+variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁]
+variable [Module R M₂]
+
+variable (R A) in
+/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products.
+
+Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra
+over the ring in which the right bilinear form is valued. -/
+def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) :=
+  ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap
+    ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm
+    ≪≫ₗ LinearMap.toBilin).toLinearMap
+  ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _
+  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
+    (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv A _ _ _)
     (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap
 #align bilin_form.tensor_distrib BilinForm.tensorDistrib
 
+-- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for
+-- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306.
 @[simp]
-theorem tensorDistrib_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂)
+theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂)
     (m₁' : M₁) (m₂' : M₂) :
-    tensorDistrib (R := R) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' :=
+    tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂')
+      = B₂ m₂ m₂' • B₁ m₁ m₁' :=
   rfl
-#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmul
+#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ
 
 /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
 @[reducible]
-protected def tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) : BilinForm R (M₁ ⊗[R] M₂) :=
-  tensorDistrib (R := R) (B₁ ⊗ₜ[R] B₂)
+protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) :=
+  tensorDistrib R A (B₁ ⊗ₜ[R] B₂)
 #align bilin_form.tmul BilinForm.tmul
 
 attribute [ext] TensorProduct.ext in
 /-- A tensor product of symmetric bilinear forms is symmetric. -/
-lemma IsSymm.tmul {B₁ : BilinForm R M₁} {B₂ : BilinForm R M₂}
+lemma IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂}
     (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by
   rw [isSymm_iff_flip R]
   apply toLin.injective
   ext x₁ x₂ y₁ y₂
-  exact (congr_arg₂ (HMul.hMul) (hB₁ x₁ y₁) (hB₂ x₂ y₂)).symm
+  exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm
+
+variable (A) in
+/-- The base change of a bilinear form. -/
+protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) :=
+  BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B
+
+@[simp]
+theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂)
+    (a' : A) (m₂' : M₂) :
+    B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') :=
+  rfl
+
+variable (A) in
+/-- The base change of a symmetric bilinear form is symmetric. -/
+lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm :=
+  IsSymm.tmul mul_comm hB₂
 
 end CommSemiring
 
@@ -84,6 +109,7 @@ variable [Module.Free R M₂] [Module.Finite R M₂]
 
 variable [Nontrivial R]
 
+variable (R) in
 /-- `tensorDistrib` as an equivalence. -/
 noncomputable def tensorDistribEquiv :
     BilinForm R M₁ ⊗[R] BilinForm R M₂ ≃ₗ[R] BilinForm R (M₁ ⊗[R] M₂) :=
@@ -96,10 +122,28 @@ noncomputable def tensorDistribEquiv :
   (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin
 #align bilin_form.tensor_distrib_equiv BilinForm.tensorDistribEquiv
 
+-- this is a dsimp lemma
+@[simp, nolint simpNF]
+theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂)
+    (m₁' : M₁) (m₂' : M₂) :
+    tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂')
+      = B₁ m₁ m₁' * B₂ m₂ m₂' :=
+  rfl
+
+variable (R M₁ M₂) in
+-- TODO: make this `rfl`
+@[simp]
+theorem tensorDistribEquiv_toLinearMap :
+    (tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R := by
+  ext B₁ B₂ : 3
+  apply toLin.injective
+  ext
+  exact mul_comm _ _
+
 @[simp]
 theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) :
-    tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (R := R) B :=
-  rfl
+    tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B :=
+  FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B
 #align bilin_form.tensor_distrib_equiv_apply BilinForm.tensorDistribEquiv_apply
 
 end CommRing

Mathlib/LinearAlgebra/Dual.lean

@@ -8,6 +8,7 @@ import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.SesquilinearForm
 import Mathlib.RingTheory.Finiteness
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+import Mathlib.RingTheory.TensorProduct
 
 #align_import linear_algebra.dual from "leanprover-community/mathlib"@"b1c017582e9f18d8494e5c18602a8cb4a6f843ac"
 
@@ -96,9 +97,9 @@ noncomputable section
 namespace Module
 
 -- Porting note: max u v universe issues so name and specific below
-universe u v v' v'' w u₁ u₂
+universe u uA v v' v'' w u₁ u₂
 
-variable (R : Type u) (M : Type v)
+variable (R : Type u) (A : Type uA) (M : Type v)
 
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
@@ -1566,7 +1567,7 @@ end VectorSpace
 
 namespace TensorProduct
 
-variable (R : Type*) (M : Type*) (N : Type*)
+variable (R A : Type*) (M : Type*) (N : Type*)
 
 variable {ι κ : Type*}
 
@@ -1608,6 +1609,24 @@ theorem dualDistrib_apply (f : Dual R M) (g : Dual R N) (m : M) (n : N) :
 
 end
 
+namespace AlgebraTensorModule
+variable [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N]
+
+variable [Module R M] [Module A M] [Module R N] [IsScalarTower R A M]
+
+/-- Heterobasic version of `TensorProduct.dualDistrib` -/
+def dualDistrib : Dual A M ⊗[R] Dual R N →ₗ[A] Dual A (M ⊗[R] N) :=
+  compRight (Algebra.TensorProduct.rid R A A) ∘ₗ homTensorHomMap R A A M N A R
+
+variable {R M N}
+
+@[simp]
+theorem dualDistrib_apply (f : Dual A M) (g : Dual R N) (m : M) (n : N) :
+    dualDistrib R A M N (f ⊗ₜ g) (m ⊗ₜ n) = g n • f m :=
+  rfl
+
+end AlgebraTensorModule
+
 variable {R M N}
 
 variable [CommRing R] [AddCommGroup M] [AddCommGroup N]