chore: refactor Submodule.baseChange (#26019)

Author: kckennylau

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -6,9 +6,10 @@ Authors: Jujian Zhang
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Limits
-import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.CategoryTheory.Adjunction.Mates
 import Mathlib.CategoryTheory.Linear.LinearFunctor
+import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 /-!
 # Change Of Rings

Mathlib/Algebra/Lie/BaseChange.lean

@@ -5,8 +5,6 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Lie.TensorProduct
-import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # Extension and restriction of scalars for Lie algebras and Lie modules
@@ -165,16 +163,14 @@ 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,
-        Submodule.mem_toAddSubmonoid] at hm ⊢
+      rw [Submodule.mem_carrier, SetLike.mem_coe] at hm ⊢
+      rw [Submodule.baseChange_eq_span] at hm
       obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm
       refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)
       · change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
         simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_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).baseChange A by
-          exact Submodule.sum_mem _ fun n _ ↦ Submodule.smul_mem _ _ (this n)
-        rintro ⟨-, ⟨n : M, hn : n ∈ N, rfl⟩⟩
+        refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_
+        rw [Subtype.coe_mk, ← h]
         exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)
       · rw [add_lie]
         exact ((N : Submodule R M).baseChange A).add_mem hy hz }
@@ -193,8 +189,8 @@ lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ N) :
 
 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
+    m ∈ Submodule.span A ((N : Submodule R M).map (TensorProduct.mk R A M 1)) := by
+  rw [← Submodule.baseChange_eq_span]; rfl
 
 @[simp]
 lemma baseChange_bot : (⊥ : LieSubmodule R L M).baseChange A = ⊥ := by
@@ -219,30 +215,11 @@ lemma lie_baseChange {I : LieIdeal R L} {N : LieSubmodule R L M} :
     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.baseChange A, ⁅x', m'⁆ ∈ Submodule.span A s) (hx := 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) (hx := hm)
-      · rintro - ⟨m', hm' : m' ∈ N, rfl⟩
-        rw [TensorProduct.mk_apply, LieAlgebra.ExtendScalars.bracket_tmul, mul_one]
-        apply Submodule.subset_span
-        exact ⟨y, hy, m', hm', rfl⟩
-      · simp
-      · intro u v _ _ hu hv
-        rw [lie_add]
-        exact Submodule.add_mem _ hu hv
-      · intro a u _ hu
-        rw [lie_smul]
-        exact Submodule.smul_mem _ a hu
-    · simp
-    · intro x y _ _ hx hy m' hm'
-      rw [add_lie]
-      exact Submodule.add_mem _ (hx _ hm') (hy _ hm')
-    · intro a x _ hx m' hm'
-      rw [smul_lie]
-      exact Submodule.smul_mem _ a (hx _ hm')
+    rw [mem_baseChange_iff] at hx hm
+    refine Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s)
+      ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx hm
+    · rintro - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩; exact Submodule.subset_span ⟨x, hx, y, hy, by simp⟩
+    all_goals { intros; simp [add_mem, Submodule.smul_mem, *] }
 
 end LieSubmodule
 

Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

@@ -3,9 +3,9 @@ Copyright (c) 2024 Jz Pan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jz Pan
 -/
-import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.Algebra.Algebra.Operations
 import Mathlib.Algebra.Algebra.Subalgebra.Lattice
+import Mathlib.LinearAlgebra.DirectSum.Finsupp
 
 /-!
 

Mathlib/LinearAlgebra/TensorProduct/Tower.lean

@@ -35,6 +35,7 @@ In this file, we use the convention that `M`, `N`, `P`, `Q` are all `R`-modules,
 * `TensorProduct.AlgebraTensorModule.leftComm`
 * `TensorProduct.AlgebraTensorModule.rightComm`
 * `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm`
+* `LinearMap.baseChange A f` is the `A`-linear map `A ⊗ f`, for an `R`-linear map `f`.
 
 ## Implementation notes
 
@@ -576,6 +577,116 @@ end AlgebraTensorModule
 
 end TensorProduct
 
+namespace LinearMap
+
+open TensorProduct
+
+/-!
+### The base-change of a linear map of `R`-modules to a linear map of `A`-modules
+-/
+
+
+section Semiring
+
+variable {R A B M N P : Type*} [CommSemiring R]
+variable [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
+variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
+variable [Module R M] [Module R N] [Module R P]
+variable (r : R) (f g : M →ₗ[R] N)
+
+variable (A) in
+/-- `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
+
+@[simp]
+theorem baseChange_tmul (a : A) (x : M) : f.baseChange A (a ⊗ₜ x) = a ⊗ₜ f x :=
+  rfl
+
+theorem baseChange_eq_ltensor : (f.baseChange A : A ⊗ M → A ⊗ N) = f.lTensor A :=
+  rfl
+
+@[simp]
+theorem baseChange_add : (f + g).baseChange A = f.baseChange A + g.baseChange A := by
+  ext
+  -- Porting note: added `-baseChange_tmul`
+  simp [baseChange_eq_ltensor, -baseChange_tmul]
+
+@[simp]
+theorem baseChange_zero : baseChange A (0 : M →ₗ[R] N) = 0 := by
+  ext
+  simp [baseChange_eq_ltensor]
+
+@[simp]
+theorem baseChange_smul : (r • f).baseChange A = r • f.baseChange A := by
+  ext
+  simp [baseChange_tmul]
+
+@[simp]
+lemma baseChange_id : (.id : M →ₗ[R] M).baseChange A = .id := by
+  ext; simp
+
+lemma baseChange_comp (g : N →ₗ[R] P) :
+    (g ∘ₗ f).baseChange A = g.baseChange A ∘ₗ f.baseChange A := by
+  ext; simp
+
+variable (R M) in
+@[simp]
+lemma baseChange_one : (1 : Module.End R M).baseChange A = 1 := baseChange_id
+
+lemma baseChange_mul (f g : Module.End R M) :
+    (f * g).baseChange A = f.baseChange A * g.baseChange A := by
+  ext; simp
+
+variable (R A M N)
+
+/-- `baseChange A e` for `e : M ≃ₗ[R] N` is the `A`-linear map `A ⊗[R] M ≃ₗ[A] A ⊗[R] N`. -/
+def _root_.LinearEquiv.baseChange (e : M ≃ₗ[R] N) : A ⊗[R] M ≃ₗ[A] A ⊗[R] N :=
+  AlgebraTensorModule.congr (.refl _ _) e
+
+/-- `baseChange` as a linear map.
+
+When `M = N`, this is true more strongly as `Module.End.baseChangeHom`. -/
+@[simps]
+def baseChangeHom : (M →ₗ[R] N) →ₗ[R] A ⊗[R] M →ₗ[A] A ⊗[R] N where
+  toFun := baseChange A
+  map_add' := baseChange_add
+  map_smul' := baseChange_smul
+
+/-- `baseChange` as an `AlgHom`. -/
+@[simps!]
+def _root_.Module.End.baseChangeHom : Module.End R M →ₐ[R] Module.End A (A ⊗[R] M) :=
+  .ofLinearMap (LinearMap.baseChangeHom _ _ _ _) (baseChange_one _ _) baseChange_mul
+
+lemma baseChange_pow (f : Module.End R M) (n : ℕ) :
+    (f ^ n).baseChange A = f.baseChange A ^ n :=
+  map_pow (Module.End.baseChangeHom _ _ _) f n
+
+end Semiring
+
+section Ring
+
+variable {R A B M N : Type*} [CommRing R]
+variable [Ring A] [Algebra R A] [Ring B] [Algebra R B]
+variable [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+variable (f g : M →ₗ[R] N)
+
+@[simp]
+theorem baseChange_sub : (f - g).baseChange A = f.baseChange A - g.baseChange A := by
+  ext
+  simp [baseChange_eq_ltensor, tmul_sub]
+
+@[simp]
+theorem baseChange_neg : (-f).baseChange A = -f.baseChange A := by
+  ext
+  simp [baseChange_eq_ltensor, tmul_neg]
+
+end Ring
+
+end LinearMap
+
 namespace Submodule
 
 open TensorProduct
@@ -588,42 +699,34 @@ 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)
+  LinearMap.range (p.subtype.baseChange A)
+
+variable {A p} in
+lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ p) :
+    a ⊗ₜ[R] m ∈ p.baseChange A :=
+  ⟨a ⊗ₜ[R] ⟨m, hm⟩, rfl⟩
+
+lemma baseChange_eq_span : p.baseChange A = span A (p.map (TensorProduct.mk R A M 1)) := by
+  refine le_antisymm ?_ ?_
+  · rw [baseChange, LinearMap.range_le_iff_comap, eq_top_iff,
+      ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..), span_le]
+    refine fun _ ⟨a, m, h⟩ ↦ ?_
+    rw [← h, SetLike.mem_coe, mem_comap, LinearMap.baseChange_tmul, ← mul_one a, ← smul_eq_mul,
+      ← smul_tmul']
+    exact smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)
+  · refine span_le.2 fun _ ⟨m, hm, h⟩ ↦ h ▸ ⟨1 ⊗ₜ[R] ⟨m, hm⟩, rfl⟩
 
 @[simp]
-lemma baseChange_bot : (⊥ : Submodule R M).baseChange A = ⊥ := by simp [baseChange]
+lemma baseChange_bot : (⊥ : Submodule R M).baseChange A = ⊥ := by simp [baseChange_eq_span]
 
 @[simp]
 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_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 (baseChange A p) a (subset_span ⟨m, hm, rfl⟩)
+  rw [eq_top_iff, ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..)]
+  exact span_le.2 fun _ ⟨a, m, h⟩ ↦ h ▸ tmul_mem_baseChange_of_mem _ trivial
 
 @[simp]
 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))
-    (hx := hm)
-  · intro m hm
-    exact subset_span ⟨m, hm, rfl⟩
-  · simp
-  · intro m₁ m₂ _ _ hm₁ hm₂
-    rw [tmul_add]
-    exact Submodule.add_mem _ hm₁ hm₂
-  · intro r m' _ hm'
-    rw [tmul_smul, ← one_smul A ((1 : A) ⊗ₜ[R] m'), ← smul_assoc]
-    exact smul_mem _ (r • 1) hm'
+  rw [baseChange_eq_span, map_span, span_span_of_tower]
 
 end Submodule