chore: delete LinearMap.extendScalars which duplicates `LinearMap.b…

…aseChange` (#8617)

For consistency, we also rename `Submodule.extendScalars` to `Submodule.baseChange` and likewise for `LieSubmodule`.

Mathlib/Algebra/Lie/BaseChange.lean

@@ -6,6 +6,7 @@ Authors: Oliver Nash
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Lie.TensorProduct
 import Mathlib.LinearAlgebra.TensorProduct.Tower
+import Mathlib.RingTheory.TensorProduct
 
 #align_import algebra.lie.base_change from "leanprover-community/mathlib"@"9264b15ee696b7ca83f13c8ad67c83d6eb70b730"
 
@@ -152,8 +153,8 @@ variable [CommRing R] [LieRing L] [LieAlgebra R L]
   [CommRing A] [Algebra R A]
 
 @[simp]
-lemma LieModule.toEndomorphism_extendScalars (x : L) :
-    toEndomorphism A (A ⊗[R] L) (A ⊗[R] M) (1 ⊗ₜ x) = (toEndomorphism R L M x).extendScalars A := by
+lemma LieModule.toEndomorphism_baseChange (x : L) :
+    toEndomorphism A (A ⊗[R] L) (A ⊗[R] M) (1 ⊗ₜ x) = (toEndomorphism R L M x).baseChange A := by
   ext; simp
 
 namespace LieSubmodule
@@ -164,9 +165,11 @@ open LieModule
 
 variable {R L M} in
 /-- If `A` is an `R`-algebra, any Lie submodule of a Lie module `M` with coefficients in `R` may be
-pushed forward to a Lie submodule of `A ⊗ M` with coefficients in `A`. -/
-def extendScalars : LieSubmodule A (A ⊗[R] L) (A ⊗[R] M) :=
-  { (N : Submodule R M).extendScalars A with
+pushed forward to a Lie submodule of `A ⊗ M` with coefficients in `A`.
+
+This "base change" operation is also known as "extension of scalars". -/
+def baseChange : LieSubmodule A (A ⊗[R] L) (A ⊗[R] M) :=
+  { (N : Submodule R M).baseChange A with
     lie_mem := by
       intro x m hm
       simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
@@ -176,56 +179,56 @@ def extendScalars : LieSubmodule A (A ⊗[R] L) (A ⊗[R] M) :=
       · change toEndomorphism A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
         simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum, map_smul, toEndomorphism_apply_apply]
         suffices ∀ n : (N : Submodule R M).map (TensorProduct.mk R A M 1),
-            ⁅a ⊗ₜ[R] y, (n : A ⊗[R] M)⁆ ∈ (N : Submodule R M).extendScalars A by
+            ⁅a ⊗ₜ[R] y, (n : A ⊗[R] M)⁆ ∈ (N : Submodule R M).baseChange A by
           exact Submodule.sum_mem _ fun n _ ↦ Submodule.smul_mem _ _ (this n)
         rintro ⟨-, ⟨n : M, hn : n ∈ N, rfl⟩⟩
-        exact Submodule.tmul_mem_extendScalars_of_mem _ (N.lie_mem hn)
+        exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)
       · rw [add_lie]
-        exact ((N : Submodule R M).extendScalars A).add_mem hy hz }
+        exact ((N : Submodule R M).baseChange A).add_mem hy hz }
 
 @[simp]
-lemma coe_extendScalars :
-    (N.extendScalars A : Submodule A (A ⊗[R] M)) = (N : Submodule R M).extendScalars A :=
+lemma coe_baseChange :
+    (N.baseChange A : Submodule A (A ⊗[R] M)) = (N : Submodule R M).baseChange A :=
   rfl
 
 variable {N}
 
 variable {R A L M} in
-lemma tmul_mem_extendScalars_of_mem (a : A) {m : M} (hm : m ∈ N) :
-    a ⊗ₜ[R] m ∈ N.extendScalars A :=
-  (N : Submodule R M).tmul_mem_extendScalars_of_mem a hm
+lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ N) :
+    a ⊗ₜ[R] m ∈ N.baseChange A :=
+  (N : Submodule R M).tmul_mem_baseChange_of_mem a hm
 
-lemma mem_extendScalars_iff {m : A ⊗[R] M} :
-    m ∈ N.extendScalars A ↔
+lemma mem_baseChange_iff {m : A ⊗[R] M} :
+    m ∈ N.baseChange A ↔
     m ∈ Submodule.span A ((N : Submodule R M).map (TensorProduct.mk R A M 1)) :=
   Iff.rfl
 
 @[simp]
-lemma extendScalars_bot : (⊥ : LieSubmodule R L M).extendScalars A = ⊥ := by
-  simp only [extendScalars, bot_coeSubmodule, Submodule.extendScalars_bot,
+lemma baseChange_bot : (⊥ : LieSubmodule R L M).baseChange A = ⊥ := by
+  simp only [baseChange, bot_coeSubmodule, Submodule.baseChange_bot,
     Submodule.bot_toAddSubmonoid]
   rfl
 
 @[simp]
-lemma extendScalars_top : (⊤ : LieSubmodule R L M).extendScalars A = ⊤ := by
-  simp only [extendScalars, top_coeSubmodule, Submodule.extendScalars_top,
+lemma baseChange_top : (⊤ : LieSubmodule R L M).baseChange A = ⊤ := by
+  simp only [baseChange, top_coeSubmodule, Submodule.baseChange_top,
     Submodule.bot_toAddSubmonoid]
   rfl
 
-lemma lie_extendScalars {I : LieIdeal R L} {N : LieSubmodule R L M} :
-    ⁅I, N⁆.extendScalars A = ⁅I.extendScalars A, N.extendScalars A⁆ := by
+lemma lie_baseChange {I : LieIdeal R L} {N : LieSubmodule R L M} :
+    ⁅I, N⁆.baseChange A = ⁅I.baseChange A, N.baseChange A⁆ := by
   set s : Set (A ⊗[R] M) := { m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ ⁅x, n⁆ = m}
   have : (TensorProduct.mk R A M 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s := by ext; simp
-  rw [← coe_toSubmodule_eq_iff, coe_extendScalars, lieIdeal_oper_eq_linear_span',
-    Submodule.extendScalars_span, this, lieIdeal_oper_eq_linear_span']
+  rw [← coe_toSubmodule_eq_iff, coe_baseChange, lieIdeal_oper_eq_linear_span',
+    Submodule.baseChange_span, this, lieIdeal_oper_eq_linear_span']
   refine le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)
   · rintro - ⟨x, hx, m, hm, rfl⟩
-    exact ⟨1 ⊗ₜ x, tmul_mem_extendScalars_of_mem 1 hx,
-           1 ⊗ₜ m, tmul_mem_extendScalars_of_mem 1 hm, by simp⟩
+    exact ⟨1 ⊗ₜ x, tmul_mem_baseChange_of_mem 1 hx,
+           1 ⊗ₜ m, tmul_mem_baseChange_of_mem 1 hm, by simp⟩
   · rintro - ⟨x, hx, m, hm, rfl⟩
     revert m
     apply Submodule.span_induction
-      (p := fun x' ↦ ∀ m' ∈ N.extendScalars A, ⁅x', m'⁆ ∈ Submodule.span A s) hx
+      (p := fun x' ↦ ∀ m' ∈ N.baseChange A, ⁅x', m'⁆ ∈ Submodule.span A s) hx
     · rintro _ ⟨y : L, hy : y ∈ I, rfl⟩ m hm
       apply Submodule.span_induction (p := fun m' ↦ ⁅(1 : A) ⊗ₜ[R] y, m'⁆ ∈ Submodule.span A s) hm
       · rintro - ⟨m', hm' : m' ∈ N, rfl⟩

Mathlib/Algebra/Lie/Killing.lean

@@ -238,12 +238,12 @@ lemma lowerCentralSeries_one_inf_center_le_ker_traceForm :
     have _i : NoZeroSMulDivisors R A := NoZeroSMulDivisors.trans R (FractionRing R) A
     rw [← map_zero (algebraMap R A)] at this
     exact NoZeroSMulDivisors.algebraMap_injective R A this
-  rw [← LinearMap.trace_extendScalars, LinearMap.extendScalars_comp, ← toEndomorphism_extendScalars,
-    ← toEndomorphism_extendScalars]
+  rw [← LinearMap.trace_baseChange, LinearMap.baseChange_comp, ← toEndomorphism_baseChange,
+    ← toEndomorphism_baseChange]
   replace hz : 1 ⊗ₜ z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1 := by
     simp only [lowerCentralSeries_succ, lowerCentralSeries_zero] at hz ⊢
-    rw [← LieSubmodule.extendScalars_top, ← LieSubmodule.lie_extendScalars]
-    exact Submodule.tmul_mem_extendScalars_of_mem 1 hz
+    rw [← LieSubmodule.baseChange_top, ← LieSubmodule.lie_baseChange]
+    exact Submodule.tmul_mem_baseChange_of_mem 1 hz
   replace hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L) := by
     simp only [mem_maxTrivSubmodule] at hzc ⊢
     intro y

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -866,11 +866,11 @@ variable (R A L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
   [CommRing A] [Algebra R A]
 
 @[simp]
-lemma LieSubmodule.lowerCentralSeries_tensor_eq_extendScalars (k : ℕ) :
+lemma LieSubmodule.lowerCentralSeries_tensor_eq_baseChange (k : ℕ) :
     lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k =
-    (lowerCentralSeries R L M k).extendScalars A := by
+    (lowerCentralSeries R L M k).baseChange A := by
   induction' k with k ih; simp
-  simp only [lowerCentralSeries_succ, ih, ← extendScalars_top, lie_extendScalars]
+  simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]
 
 instance LieModule.instIsNilpotentTensor [IsNilpotent R L M] :
     IsNilpotent A (A ⊗[R] L) (A ⊗[R] M) := by

Mathlib/LinearAlgebra/TensorProduct/Tower.lean

@@ -451,30 +451,6 @@ end AlgebraTensorModule
 
 end TensorProduct
 
-namespace LinearMap
-
-open TensorProduct
-
-variable {R M₁ M₂ M₃ : Type*} (A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
-  [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃]
-  (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃)
-
-/-- If `A` is an `R`-algebra, any `R`-linear map `M₁ → M₂` naturally induces an `A`-linear map
-`A ⊗ M₁ → A ⊗ M₂`. -/
-def extendScalars : A ⊗[R] M₁ →ₗ[A] A ⊗[R] M₂ :=
-  TensorProduct.AlgebraTensorModule.map LinearMap.id f
-
-@[simp]
-lemma extendScalars_tmul (a : A) (m : M₁) :
-    f.extendScalars A (a ⊗ₜ m) = a ⊗ₜ f m :=
-  rfl
-
-lemma extendScalars_comp :
-    (g ∘ₗ f).extendScalars A = g.extendScalars A ∘ₗ f.extendScalars A := by
-  ext; simp
-
-end LinearMap
-
 namespace Submodule
 
 open TensorProduct
@@ -483,32 +459,34 @@ variable {R M : Type*} (A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
   [AddCommMonoid M] [Module R M] (p : Submodule R M)
 
 /-- If `A` is an `R`-algebra, any `R`-submodule `p` of an `R`-module `M` may be pushed forward to
-an `A`-submodule of `A ⊗ M`. -/
-def extendScalars : Submodule A (A ⊗[R] M) :=
+an `A`-submodule of `A ⊗ M`.
+
+This "base change" operation is also known as "extension of scalars". -/
+def baseChange : Submodule A (A ⊗[R] M) :=
   span A <| p.map (TensorProduct.mk R A M 1)
 
 @[simp]
-lemma extendScalars_bot : (⊥ : Submodule R M).extendScalars A = ⊥ := by simp [extendScalars]
+lemma baseChange_bot : (⊥ : Submodule R M).baseChange A = ⊥ := by simp [baseChange]
 
 @[simp]
-lemma extendScalars_top : (⊤ : Submodule R M).extendScalars A = ⊤ := by
-  rw [extendScalars, map_top, eq_top_iff']
+lemma baseChange_top : (⊤ : Submodule R M).baseChange A = ⊤ := by
+  rw [baseChange, map_top, eq_top_iff']
   intro x
   refine x.induction_on (by simp) (fun a y ↦ ?_) (fun _ _ ↦ Submodule.add_mem _)
   rw [← mul_one a, ← smul_eq_mul, ← smul_tmul']
   refine smul_mem _ _ (subset_span ?_)
   simp
 
 variable {A p} in
-lemma tmul_mem_extendScalars_of_mem (a : A) {m : M} (hm : m ∈ p) :
-    a ⊗ₜ[R] m ∈ p.extendScalars A := by
+lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ p) :
+    a ⊗ₜ[R] m ∈ p.baseChange A := by
   rw [← mul_one a, ← smul_eq_mul, ← smul_tmul']
-  exact smul_mem (extendScalars A p) a (subset_span ⟨m, hm, rfl⟩)
+  exact smul_mem (baseChange A p) a (subset_span ⟨m, hm, rfl⟩)
 
 @[simp]
-lemma extendScalars_span (s : Set M) :
-    (span R s).extendScalars A = span A (TensorProduct.mk R A M 1 '' s) := by
-  simp only [extendScalars, map_coe]
+lemma baseChange_span (s : Set M) :
+    (span R s).baseChange A = span A (TensorProduct.mk R A M 1 '' s) := by
+  simp only [baseChange, map_coe]
   refine le_antisymm (span_le.mpr ?_) (span_mono <| Set.image_subset _ subset_span)
   rintro - ⟨m : M, hm : m ∈ span R s, rfl⟩
   apply span_induction (p := fun m' ↦ (1 : A) ⊗ₜ[R] m' ∈ span A (TensorProduct.mk R A M 1 '' s)) hm

Mathlib/LinearAlgebra/Trace.lean

@@ -329,9 +329,9 @@ lemma trace_comp_eq_mul_of_commute_of_isNilpotent [IsReduced R] {f g : Module.En
   rw [hμ, comp_add, map_add, hg, add_zero, this, LinearMap.map_smul, smul_eq_mul]
 
 @[simp]
-lemma trace_extendScalars [Module.Free R M] [Module.Finite R M]
+lemma trace_baseChange [Module.Free R M] [Module.Finite R M]
     (f : M →ₗ[R] M) (A : Type*) [CommRing A] [Algebra R A] :
-    trace A _ (f.extendScalars A) = algebraMap R A (trace R _ f) := by
+    trace A _ (f.baseChange A) = algebraMap R A (trace R _ f) := by
   let b := Module.Free.chooseBasis R M
   let b' := Algebra.TensorProduct.basis A b
   change _ = (algebraMap R A : R →+ A) _

Mathlib/RingTheory/TensorProduct.lean

@@ -64,7 +64,9 @@ variable (r : R) (f g : M →ₗ[R] N)
 
 variable (A)
 
-/-- `baseChange A f` for `f : M →ₗ[R] N` is the `A`-linear map `A ⊗[R] M →ₗ[A] A ⊗[R] N`. -/
+/-- `baseChange A f` for `f : M →ₗ[R] N` is the `A`-linear map `A ⊗[R] M →ₗ[A] A ⊗[R] N`.
+
+This "base change" operation is also known as "extension of scalars". -/
 def baseChange (f : M →ₗ[R] N) : A ⊗[R] M →ₗ[A] A ⊗[R] N :=
   AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) f
 #align linear_map.base_change LinearMap.baseChange
@@ -99,6 +101,10 @@ theorem baseChange_smul : (r • f).baseChange A = r • f.baseChange A := by
   simp [baseChange_tmul]
 #align linear_map.base_change_smul LinearMap.baseChange_smul
 
+lemma baseChange_comp {P : Type*} [AddCommMonoid P] [Module R P] (g : N →ₗ[R] P) :
+    (g ∘ₗ f).baseChange A = g.baseChange A ∘ₗ f.baseChange A := by
+  ext; simp
+
 variable (R A M N)
 
 /-- `baseChange` as a linear map. -/
@@ -1109,8 +1115,8 @@ variable {R M₁ M₂ ι ι₂ : Type*} (A : Type*)
   [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
 
 @[simp]
-lemma toMatrix_extendScalars (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) :
-    toMatrix (basis A b₁) (basis A b₂) (f.extendScalars A) =
+lemma toMatrix_baseChange (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) :
+    toMatrix (basis A b₁) (basis A b₂) (f.baseChange A) =
     (toMatrix b₁ b₂ f).map (algebraMap R A) := by
   ext; simp [toMatrix_apply]