refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps

Mathlib/LinearAlgebra/BilinearForm/Hom.lean

@@ -39,6 +39,7 @@ Bilinear form,
 -/
 
 open LinearMap (BilinForm)
+open LinearMap (BilinMap)
 
 universe u v w
 
@@ -305,6 +306,25 @@ theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R
       B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) :=
   rfl
 
+variable {N₁ N₂ : Type*}
+variable [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂]
+
+/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear
+maps into `N₂`. -/
+@[simps]
+def _root_.LinearMap.BilinMap.congr₂ (e : N₁ ≃ₗ[R] N₂) : BilinMap R M N₁ ≃ₗ[R] BilinMap R M N₂ where
+  toFun B := LinearMap.compr₂ B e
+  invFun B := LinearMap.compr₂ B e.symm
+  left_inv B := ext₂ fun x => by
+    simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, implies_true]
+  right_inv B := ext₂ fun x => by
+    simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, implies_true]
+  map_add' B B' := ext₂ fun x y => by
+    simp only [compr₂_apply, LinearMap.add_apply, map_add, LinearEquiv.coe_coe]
+  map_smul' B B' := ext₂ fun x y => by
+    simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe,
+      RingHom.id_apply]
+
 end congr
 
 section LinMulLin

Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.TensorProduct.Tower
+import Mathlib.LinearAlgebra.BilinearForm.Hom
 
 /-!
 # The bilinear form on a tensor product
@@ -20,9 +21,10 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 suppress_compilation
 
-universe u v w uι uR uA uM₁ uM₂
+universe u v w uι uR uA uM₁ uM₂ uN₁ uN₂
 
-variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂}
+variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁}
+  {N₂ : Type uN₂}
 
 open TensorProduct
 
@@ -35,23 +37,48 @@ open LinearMap (BilinForm)
 
 section CommSemiring
 variable [CommSemiring R] [CommSemiring A]
-variable [AddCommMonoid M₁] [AddCommMonoid M₂]
-variable [Algebra R A] [Module R M₁] [Module A M₁]
+variable [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂]
+variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁]
 variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁]
-variable [Module R M₂]
+variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁]
+variable [Module R M₂] [Module R N₂]
+
+variable (R A) in
+/-- The tensor product of two bilinear maps injects into bilinear maps on tensor products.
+
+Note this is heterobasic; the bilinear map on the left can take values in a module over a
+(commutative) algebra over the ring of the module in which the right bilinear map is valued. -/
+def tensorDistrib' :
+    ((BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂)) →ₗ[A] ((BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))) :=
+  (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ
+ ((LinearMap.llcomp A _ _ _).flip
+   (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap)
+  ∘ₗ TensorProduct.AlgebraTensorModule.homTensorHomMap R _ _ _ _ _ _
+  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
+    (TensorProduct.lift.equiv A M₁ M₁ N₁)
+    (TensorProduct.lift.equiv R _ _ _)).toLinearMap
+
+@[simp]
+theorem tensorDistrib_tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂)
+    (m₁' : M₁) (m₂' : M₂) :
+    tensorDistrib' R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂')
+      = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' :=
+  rfl
+
+/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
+protected abbrev tmul' (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap  R M₂ N₂) :
+    BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
+  tensorDistrib' R A (B₁ ⊗ₜ[R] B₂)
 
 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).toLinearMap
-  ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _
-  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
-    (TensorProduct.lift.equiv A M₁ M₁ A)
-    (TensorProduct.lift.equiv R _ _ _)).toLinearMap
+  (congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A)
+
+variable (R A) in
 
 -- 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.

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -585,6 +585,23 @@ def _root_.LinearMap.compQuadraticMap' [CommSemiring S] [Algebra S R] [Module S
     (f : N →ₗ[S] P) (Q : QuadraticMap R M N) : QuadraticMap S M P :=
   _root_.LinearMap.compQuadraticMap f Q.restrictScalars
 
+
+/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear
+maps into `N₂`. -/
+@[simps]
+def congr₂ (e : N ≃ₗ[R] P) : QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P where
+  toFun Q := e.compQuadraticMap Q
+  invFun Q := e.symm.compQuadraticMap Q
+  left_inv _ := ext fun x => by
+    simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply]
+  right_inv _ := ext fun x => by
+    simp only [LinearMap.compQuadraticMap_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply]
+  map_add' _ _ := ext fun x => by
+    simp only [LinearMap.compQuadraticMap_apply, add_apply, map_add, LinearEquiv.coe_coe]
+  map_smul' _ _ := ext fun x => by
+    simp only [LinearMap.compQuadraticMap_apply, smul_apply, LinearMapClass.map_smul,
+      LinearEquiv.coe_coe, RingHom.id_apply]
+
 end Comp
 section NonUnitalNonAssocSemiring
 
@@ -874,12 +891,12 @@ theorem toQuadraticMap_associated : (associatedHom S Q).toQuadraticMap = Q :=
 -- note: usually `rightInverse` lemmas are named the other way around, but this is consistent
 -- with historical naming in this file.
 theorem associated_rightInverse :
-    Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M R) :=
+    Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M N) :=
   fun Q => toQuadraticMap_associated S Q
 
 /-- `associated'` is the `ℤ`-linear map that sends a quadratic form on a module `M` over `R` to its
 associated symmetric bilinear form. -/
-abbrev associated' : QuadraticMap R M R →ₗ[ℤ] BilinMap R M R :=
+abbrev associated' : QuadraticMap R M N →ₗ[ℤ] BilinMap R M N :=
   associatedHom ℤ
 
 /-- Symmetric bilinear forms can be lifted to quadratic forms -/
@@ -889,9 +906,9 @@ instance canLift :
 
 /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated
 bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/
-theorem exists_quadraticForm_ne_zero {Q : QuadraticForm R M}
+theorem exists_quadraticForm_ne_zero {Q : QuadraticMap R M N}
     -- Porting note: added implicit argument
-    (hB₁ : associated' (R := R) Q ≠ 0) :
+    (hB₁ : associated' (R := R) (N := N) Q ≠ 0) :
     ∃ x, Q x ≠ 0 := by
   rw [← not_forall]
   intro h
@@ -1024,7 +1041,7 @@ variable [CommRing R] [AddCommGroup M] [Module R M]
 theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticMap R M R)
     (hB : Q.Anisotropic) :
     -- Porting note: added implicit argument
-    (QuadraticMap.associated' (R := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by
+    (QuadraticMap.associated' (R := R) (N := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by
   rw [← hx x]
   exact (associated_eq_self_apply _ _ x).symm
 

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

@@ -16,9 +16,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic
 
 -/
 
-universe uR uA uM₁ uM₂
+universe uR uA uM₁ uM₂ uN₁ uN₂
 
-variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂}
+variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂}
 
 open TensorProduct
 open LinearMap (BilinMap)
@@ -29,18 +29,51 @@ namespace QuadraticForm
 
 section CommRing
 variable [CommRing R] [CommRing A]
-variable [AddCommGroup M₁] [AddCommGroup M₂]
-variable [Algebra R A] [Module R M₁] [Module A M₁]
+variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂]
+variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁]
 variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁]
-variable [Module R M₂] [Invertible (2 : R)]
+variable [SMulCommClass R A N₁] [SMulCommClass A R N₁] [IsScalarTower R A N₁]
+variable [Module R M₂] [Module R N₂] [Invertible (2 : R)]
 
+variable (R A) in
+/-- The tensor product of two quadratic maps injects into quadratic maps on tensor products.
+
+Note this is heterobasic; the quadratic map on the left can take values in a module over a larger
+ring than the one on the right. -/
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def tensorDistrib' :
+    QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
+  letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
+  -- while `letI`s would produce a better term than `let`, they would make this already-slow
+  -- definition even slower.
+  let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂)
+  let tmulB := BilinMap.tensorDistrib' R A (M₁ := M₁) (M₂ := M₂)
+  let toB := AlgebraTensorModule.map
+      (QuadraticMap.associated : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁)
+      (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂)
+  toQ ∘ₗ tmulB ∘ₗ toB
+
+@[simp]
+theorem tensorDistrib_tmul' (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁)
+    (m₂ : M₂) : tensorDistrib' R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂   :=
+  letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
+  (BilinMap.tensorDistrib_tmul' _ _ _ _ _ _).trans <| congr_arg₂ _
+    (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
+
+/-- The tensor product of two quadratic maps, a shorthand for dot notation. -/
+-- `noncomputable` is a performance workaround for mathlib4#7103
+protected noncomputable abbrev _root_.QuadraticMap.tmul' (Q₁ : QuadraticMap A M₁ N₁)
+    (Q₂ : QuadraticMap R M₂ N₂) : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
+  tensorDistrib' R A (Q₁ ⊗ₜ[R] Q₂)
 
 variable (R A) in
 /-- The tensor product of two quadratic forms injects into quadratic forms on tensor products.
 
 Note this is heterobasic; the quadratic form on the left can take values in a larger ring than
 the one on the right. -/
 -- `noncomputable` is a performance workaround for mathlib4#7103
+-- Should be `(congr₂ (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib' R A)` but then
+-- `associated_tmul` breaks
 noncomputable def tensorDistrib :
     QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) :=
   letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
@@ -52,14 +85,15 @@ noncomputable def tensorDistrib :
       (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁)
       (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂)
   toQ ∘ₗ tmulB ∘ₗ toB
+--
 
 -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for
 -- `R = A` of `Q₁ m₁ * Q₂ m₂`.
 @[simp]
 theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) :
     tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ :=
   letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
-  (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _
+  (BilinMap.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <| congr_arg₂ _
     (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
 
 /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/