feat(LinearAlgebra/BilinearForm/TensorProduct): base change of bilinear forms (#6306)

This generalizes the existing `BilinForm.tensorDistrib` to be heterogenous in the rings it uses, such that a base change,
```lean
protected def baseChange (B : BilinForm R M₂) :
  BilinForm A (A ⊗[R] M₂) :=
```
falls out as a special case. I do not attempt to generalize `BilinForm.tensorDistribEquiv`.

Unfortunately, this changes the defeq as
```diff
-(B₁.tmul B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂'
+(B₁.tmul B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₂ m₂ m₂' • B₁ m₁ m₁'
```
We could fix this by using the right action instead, but that's a lot of work for a very minorly annoying defeq.

This also breaks the defeq of `tensorDistribEquiv B = tensorDistrib B`; though the reason is more complicated than the scalar action issue above. It would be fixed if we defined all the homogenous operations on tensor products as special cases of the heterogenous ones, but that's also a lot of work for a very small win.

This is a port of work from pygae/lean-ga#31, and almost at the end of the path to a base change of quadratic forms and clifford algebras.

This was independently developed at the Leiden workshop as [`BilinForm.baseChange`](https://github.com/alexjbest/ant-lorentz/blob/1f97add294b2d50f99537c15583666d78b0d7e24/AntLorentz/BaseChange.lean#L75-L85), though the results there are not sorry-free.

Author: eric-wieser

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]