feat(LinearAlgebra/BilinearMap): restrict scalars (#6133)

Generalizes the previous definition and moves it into `LinearAlgebra/BilinearMap`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -22,26 +22,6 @@ open TensorProduct Module
 
 namespace LinearMap
 
-section RestrictScalars
-
-variable
-  (R : Type*) {A M N P : Type*}
-  [CommSemiring R] [CommSemiring A]
-  [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
-  [Algebra R A]
-  [Module R M] [Module R N] [Module R P]
-  [Module A M] [Module A N] [Module A P]
-  [IsScalarTower R A M] [IsScalarTower R A N] [IsScalarTower R A P]
-
-/-- A version of `LinearMap.restrictScalars` for bilinear maps.
-
-The double subscript in the name is to match `LinearMap.compl₁₂`. -/
-@[simps!]
-def restrictScalars₁₂ (f : M →ₗ[A] N →ₗ[A] P) : M →ₗ[R] N →ₗ[R] P :=
-  (f.flip.restrictScalars _).flip.restrictScalars _
-
-end RestrictScalars
-
 section NonUnitalNonAssoc
 
 variable (R A : Type*) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A]

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -208,6 +208,42 @@ theorem domRestrict₁₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂]
     (x : p) (y : q) : f.domRestrict₁₂ p q x y = f x y := rfl
 #align linear_map.dom_restrict₁₂_apply LinearMap.domRestrict₁₂_apply
 
+section restrictScalars
+
+variable (R' S' : Type*)
+
+variable [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ]
+
+variable [SMulCommClass S' R' Pₗ]
+
+variable [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ]
+
+variable [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ]
+
+/-- If `B : M → N → Pₗ` is `R`-`S` bilinear and `R'` and `S'` are compatible scalar multiplications,
+then the restriction of scalars is a `R'`-`S'` bilinear map.-/
+@[simps!]
+def restrictScalars₁₂ (B : M →ₗ[R] N →ₗ[S] Pₗ) : M →ₗ[R'] N →ₗ[S'] Pₗ :=
+  LinearMap.mk₂' R' S'
+    (B · ·)
+    B.map_add₂
+    (fun r' m _ ↦ by
+      dsimp only
+      rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul])
+    (fun _ ↦ map_add _)
+    (fun _ x ↦ (B x).map_smul_of_tower _)
+
+theorem restrictScalars₁₂_injective : Function.Injective
+    (LinearMap.restrictScalars₁₂ R' S' : (M →ₗ[R] N →ₗ[S] Pₗ) → (M →ₗ[R'] N →ₗ[S'] Pₗ)) :=
+  fun _ _ h ↦ ext₂ (congr_fun₂ h : _)
+
+@[simp]
+theorem restrictScalars₁₂_inj {B B' : M →ₗ[R] N →ₗ[S] Pₗ} :
+    B.restrictScalars₁₂ R' S' = B'.restrictScalars₁₂ R' S' ↔ B = B' :=
+  (restrictScalars₁₂_injective R' S').eq_iff
+
+end restrictScalars
+
 end Semiring
 
 section CommSemiring

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -571,7 +571,7 @@ def _root_.LinearMap.compQuadraticForm [CommSemiring S] [Algebra S R] [Module S
   toFun_smul b x := by simp only [Q.map_smul_of_tower b x, f.map_smul, smul_eq_mul]
   exists_companion' :=
     let ⟨B, h⟩ := Q.exists_companion
-    ⟨(B.restrictScalars₁₂ S).compr₂ f, fun x y => by
+    ⟨(B.restrictScalars₁₂ S S).compr₂ f, fun x y => by
       simp_rw [h, f.map_add, LinearMap.compr₂_apply, LinearMap.restrictScalars₁₂_apply_apply]⟩
 #align linear_map.comp_quadratic_form LinearMap.compQuadraticForm
 
@@ -798,7 +798,7 @@ theorem compQuadraticForm_polar (f : R →ₗ[S] S) (Q : QuadraticForm R M) (x y
 
 theorem compQuadraticForm_polarBilin (f : R →ₗ[S] S) (Q : QuadraticForm R M) :
     (f.compQuadraticForm Q).polarBilin =
-    (Q.polarBilin.restrictScalars₁₂ S).compr₂ f :=
+    (Q.polarBilin.restrictScalars₁₂ S S).compr₂ f :=
   ext₂ <| compQuadraticForm_polar _ _
 
 end Ring