feat (LinearAlgebra/BilinearMap): restrict scalars and range of a linear map (#24345)

This PR introduces `restrictScalarsRange`, which is a linear map that restricts the scalars and range of a linear map. The function previously named `restrictScalarsRange` is about bilinear maps, and is renamed `restrictScalarsRange₂`.

Author: ScottCarnahan

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -429,6 +429,43 @@ open Function
 
 section restrictScalarsRange
 
+variable {R S M P M' P' : Type*}
+  [CommSemiring R] [CommSemiring S] [SMul S R]
+  [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P]
+  [Module S M] [Module S P]
+  [IsScalarTower S R M] [IsScalarTower S R P]
+  [AddCommMonoid M'] [Module S M'] [AddCommMonoid P'] [Module S P']
+
+variable (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Injective k)
+  (f : M →ₗ[R] P) (hf : ∀ m, f (i m) ∈ LinearMap.range k)
+
+/-- Restrict the scalars and range of a linear map. -/
+noncomputable def restrictScalarsRange :
+    M' →ₗ[S] P' :=
+  ((f.restrictScalars S).comp i).codLift k hk hf
+
+@[simp]
+lemma restrictScalarsRange_apply (m : M') :
+    k (restrictScalarsRange i k hk f hf m) = f (i m) := by
+  have : k (restrictScalarsRange i k hk f hf m) =
+      (k ∘ₗ ((f.restrictScalars S).comp i).codLift k hk hf) m :=
+    rfl
+  rw [this, comp_codLift, comp_apply, restrictScalars_apply]
+
+@[simp]
+lemma eq_restrictScalarsRange_iff (m : M') (p : P') :
+    p = restrictScalarsRange i k hk f hf m ↔ k p = f (i m) := by
+  rw [← restrictScalarsRange_apply i k hk f hf m, hk.eq_iff]
+
+@[simp]
+lemma restrictScalarsRange_apply_eq_zero_iff (m : M') :
+    restrictScalarsRange i k hk f hf m = 0 ↔ f (i m) = 0 := by
+  rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]
+
+end restrictScalarsRange
+
+section restrictScalarsRange₂
+
 variable {R S M N P M' N' P' : Type*}
   [CommSemiring R] [CommSemiring S] [SMul S R]
   [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P]
@@ -441,25 +478,25 @@ variable (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (k : P' →ₗ[S] P) (hk : In
   (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ m n, B (i m) (j n) ∈ LinearMap.range k)
 
 /-- Restrict the scalars, domains, and range of a bilinear map. -/
-noncomputable def restrictScalarsRange :
+noncomputable def restrictScalarsRange₂ :
     M' →ₗ[S] N' →ₗ[S] P' :=
   (((LinearMap.restrictScalarsₗ S R _ _ _).comp
     (B.restrictScalars S)).compl₁₂ i j).codRestrict₂ k hk hB
 
-@[simp] lemma restrictScalarsRange_apply (m : M') (n : N') :
-    k (restrictScalarsRange i j k hk B hB m n) = B (i m) (j n) := by
-  simp [restrictScalarsRange]
+@[simp] lemma restrictScalarsRange₂_apply (m : M') (n : N') :
+    k (restrictScalarsRange₂ i j k hk B hB m n) = B (i m) (j n) := by
+  simp [restrictScalarsRange₂]
 
 @[simp]
-lemma eq_restrictScalarsRange_iff (m : M') (n : N') (p : P') :
-    p = restrictScalarsRange i j k hk B hB m n ↔ k p = B (i m) (j n) := by
-  rw [← restrictScalarsRange_apply i j k hk B hB m n, hk.eq_iff]
+lemma eq_restrictScalarsRange₂_iff (m : M') (n : N') (p : P') :
+    p = restrictScalarsRange₂ i j k hk B hB m n ↔ k p = B (i m) (j n) := by
+  rw [← restrictScalarsRange₂_apply i j k hk B hB m n, hk.eq_iff]
 
 @[simp]
-lemma restrictScalarsRange_apply_eq_zero_iff (m : M') (n : N') :
-    restrictScalarsRange i j k hk B hB m n = 0 ↔ B (i m) (j n) = 0 := by
-  rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]
+lemma restrictScalarsRange₂_apply_eq_zero_iff (m : M') (n : N') :
+    restrictScalarsRange₂ i j k hk B hB m n = 0 ↔ B (i m) (j n) = 0 := by
+  rw [← hk.eq_iff, restrictScalarsRange₂_apply, map_zero]
 
-end restrictScalarsRange
+end restrictScalarsRange₂
 
 end LinearMap

Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

@@ -92,15 +92,15 @@ variable {S M' N' : Type*}
 private def restrictScalarsAux
     (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap S R).range) :
     M' →ₗ[S] N' →ₗ[S] S :=
- LinearMap.restrictScalarsRange i j (Algebra.linearMap S R)
+ LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap S R)
     (FaithfulSMul.algebraMap_injective S R) p.toLinearMap hp
 
 private lemma restrictScalarsAux_injective
     (hi : Injective i)
     (hN : span R (LinearMap.range j : Set N) = ⊤)
     (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap S R).range) :
     Injective (p.restrictScalarsAux i j hp) := by
-  let f := LinearMap.restrictScalarsRange i j (Algebra.linearMap S R)
+  let f := LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap S R)
       (FaithfulSMul.algebraMap_injective S R) p.toLinearMap hp
   rw [← LinearMap.ker_eq_bot]
   refine (Submodule.eq_bot_iff _).mpr fun x (hx : f x = 0) ↦ ?_
@@ -257,7 +257,7 @@ def restrictScalarsField
     (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap K L).range)
     (x : M') (y : N') :
     algebraMap K L (p.restrictScalarsField i j hi hj hij hp x y) = p (i x) (j y) :=
-  LinearMap.restrictScalarsRange_apply i j (Algebra.linearMap K L)
+  LinearMap.restrictScalarsRange₂_apply i j (Algebra.linearMap K L)
     (FaithfulSMul.algebraMap_injective K L) p.toLinearMap hp x y
 
 end Field

Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

@@ -138,7 +138,7 @@ lemma two_mul_apply_root_root :
 values in `S`, this is the associated `S`-bilinear form on the `S`-span of the roots. -/
 def posForm :
     LinearMap.BilinForm S (span S (range P.root)) :=
-  LinearMap.restrictScalarsRange (span S (range P.root)).subtype (span S (range P.root)).subtype
+  LinearMap.restrictScalarsRange₂ (span S (range P.root)).subtype (span S (range P.root)).subtype
   (Algebra.linearMap S R) (FaithfulSMul.algebraMap_injective S R) B.form
   (fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ by
     apply LinearMap.BilinMap.apply_apply_mem_of_mem_span