feat: base change properties, direct sums, bases, modules of linear maps (#31240)

Establish various `IsBaseChange` properties:
* direct sums commute with base change
* when the source module is finite free, modules of linear maps commute with base change (on the right, on both sides, and for endomorphisms).
* a base change of a free module is free, with compatible bases.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: AntoineChambert-Loir

Mathlib.lean

@@ -6130,6 +6130,8 @@ public import Mathlib.RingTheory.TensorProduct.Basic
 public import Mathlib.RingTheory.TensorProduct.DirectLimitFG
 public import Mathlib.RingTheory.TensorProduct.Finite
 public import Mathlib.RingTheory.TensorProduct.Free
+public import Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
+public import Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
 public import Mathlib.RingTheory.TensorProduct.IsBaseChangePi
 public import Mathlib.RingTheory.TensorProduct.Maps
 public import Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Mathlib/Algebra/DirectSum/Finsupp.lean

@@ -43,10 +43,22 @@ theorem finsuppLEquivDirectSum_single (i : ι) (m : M) :
     finsuppLEquivDirectSum R M ι (Finsupp.single i m) = DirectSum.lof R ι _ i m :=
   Finsupp.toDFinsupp_single i m
 
+@[simp]
+theorem finsuppLEquivDirectSum_apply (m : ι →₀ M) (i : ι) :
+    finsuppLEquivDirectSum R M ι m i = m i := by
+  rfl
+
 @[simp]
 theorem finsuppLEquivDirectSum_symm_lof (i : ι) (m : M) :
     (finsuppLEquivDirectSum R M ι).symm (DirectSum.lof R ι _ i m) = Finsupp.single i m :=
   letI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
   DFinsupp.toFinsupp_single i m
 
+theorem lmap_finsuppLEquivDirectSum_eq {N : Type*} [AddCommMonoid N] [Module R N]
+    (ε : M →ₗ[R] N) (m : ι →₀ M) :
+    (lmap fun _ ↦ ε) ((finsuppLEquivDirectSum R M ι) m) =
+      (finsuppLEquivDirectSum R N ι) (m.mapRange ⇑ε ε.map_zero) := by
+  ext i
+  rfl
+
 end finsuppLequivDirectSum

Mathlib/Algebra/DirectSum/Module.lean

@@ -545,4 +545,44 @@ end Ring
 
 end Submodule
 
+section Congr
+
+variable {R : Type*} [Semiring R]
+    {ι : Type*}
+    {N : ι → Type*} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)]
+    {P : ι → Type*} [∀ i, AddCommMonoid (P i)] [∀ i, Module R (P i)]
+
+/-- Direct sums of isomorphic additive groups are isomorphic. -/
+def congr_addEquiv (u : (i : ι) → N i ≃+ P i) :
+    (⨁ i, N i) ≃+ ⨁ i, P i where
+  toAddHom := DirectSum.map fun i ↦ (u i).toAddMonoidHom
+  invFun := DirectSum.map fun i ↦ (u i).symm.toAddMonoidHom
+  left_inv x := by aesop
+  right_inv y := by aesop
+
+theorem coe_congr_addEquiv (u : (i : ι) → N i ≃+ P i) :
+    ⇑(congr_addEquiv u).toAddMonoidHom = ⇑(DirectSum.map fun i ↦ (u i).toAddMonoidHom) :=
+  rfl
+
+/-- Direct sums of isomorphic modules are isomorphic. -/
+def congr_linearEquiv (u : (i : ι) → N i ≃ₗ[R] P i) :
+    (⨁ i, N i) ≃ₗ[R] ⨁ i, P i where
+  toAddEquiv := congr_addEquiv (fun i ↦ (u i).toAddEquiv)
+  map_smul' r x := by
+    exact (DirectSum.lmap (fun i ↦ (u i).toLinearMap)).map_smul r x
+
+theorem coe_congr_linearEquiv (u : (i : ι) → N i ≃ₗ[R] P i) :
+    ⇑(congr_linearEquiv u) = ⇑(DirectSum.lmap (fun i ↦ (u i).toLinearMap)) :=
+  rfl
+
+theorem congr_linearEquiv_toAddEquiv (u : (i : ι) → N i ≃ₗ[R] P i) :
+    (congr_linearEquiv u).toAddEquiv = congr_addEquiv (fun i ↦ (u i).toAddEquiv) :=
+  rfl
+
+theorem congr_linearEquiv_toLinearMap (u : (i : ι) → N i ≃ₗ[R] P i) :
+    (congr_linearEquiv u).toLinearMap = DirectSum.lmap (fun i ↦ (u i).toLinearMap) :=
+  rfl
+
+end Congr
+
 end DirectSum

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

@@ -116,6 +116,18 @@ theorem directSumLeft_symm_lof_tmul (i : ι₁) (x : M₁ i) (y : M₂') :
       DirectSum.lof R _ _ i x ⊗ₜ[R] y := by
   rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]
 
+@[simp]
+lemma directSumLeft_tmul (m : ⨁ i, M₁ i) (n : M₂') (i : ι₁) :
+    directSumLeft R M₁ M₂' (m ⊗ₜ[R] n) i = (m i) ⊗ₜ[R] n := by
+  suffices (DirectSum.component R ι₁ _ i) ∘ₗ(directSumLeft R M₁ M₂').toLinearMap ∘ₗ
+      ((TensorProduct.mk R (⨁ i, M₁ i) M₂').flip n) =
+        ((TensorProduct.mk R (M₁ i) M₂').flip n) ∘ₗ (DirectSum.component R ι₁ M₁ i) by
+    simpa using LinearMap.congr_fun this m
+  ext j n
+  by_cases hj : j = i
+  · subst hj; simp
+  · simp [DirectSum.component.of, hj]
+
 @[simp]
 theorem directSumRight_tmul_lof (x : M₁') (i : ι₂) (y : M₂ i) :
     directSumRight R M₁' M₂ (x ⊗ₜ[R] DirectSum.lof R _ _ i y) =
@@ -135,6 +147,49 @@ lemma directSumRight_comp_rTensor (f : M₁' →ₗ[R] M₂') :
       (lmap fun _ ↦ f.rTensor _) ∘ₗ directSumRight R M₁' M₁ := by
   ext; simp
 
+@[simp]
+lemma directSumRight_tmul (m : M₁') (n : ⨁ i, M₂ i) (i : ι₂) :
+    directSumRight R M₁' M₂ (m ⊗ₜ[R] n) i = m ⊗ₜ[R] (n i) := by
+  suffices (DirectSum.component R ι₂ _ i) ∘ₗ(directSumRight R M₁' M₂).toLinearMap ∘ₗ
+      (TensorProduct.mk R M₁' (⨁ i, M₂ i) m) =
+        (TensorProduct.mk R M₁' (M₂ i) m) ∘ₗ (DirectSum.component R ι₂ M₂ i) by
+    simpa using LinearMap.congr_fun this n
+  ext j n
+  by_cases hj : j = i
+  · subst hj; simp
+  · simp [DirectSum.component.of, hj]
+
+variable [Module S M₁'] [IsScalarTower R S M₁']
+
+-- NB. Why not giving `TensorProduct.directSumRight` the adequate linearity?
+variable (M₁' M₂) in
+/-- Tensor products distribute over a direct sum on the right.
+
+This version has more linearity than `TensorProduct.directSumRight`. -/
+def directSumRight' : (M₁' ⊗[R] ⨁ i, M₂ i) ≃ₗ[S] ⨁ i, M₁' ⊗[R] M₂ i where
+  toAddEquiv := (directSumRight ..).toAddEquiv
+  map_smul' s t := by
+    induction t using TensorProduct.induction_on with
+    | zero => simp
+    | add x y hx hy =>
+      simp only [AddHom.toFun_eq_coe, coe_toAddHom,
+        LinearEquiv.coe_coe, RingHom.id_apply] at hx hy ⊢
+      simp only [smul_add, map_add, hx, hy]
+    | tmul m n =>
+      simp
+      rw [TensorProduct.smul_tmul']
+      ext i
+      rw [DirectSum.smul_apply, directSumRight_tmul,
+        directSumRight_tmul, TensorProduct.smul_tmul']
+
+lemma directSumRight'_restrict :
+    (directSumRight' R S M₁' M₂).restrictScalars R = directSumRight R M₁' M₂ :=
+  rfl
+
+lemma coe_directSumRight' :
+    ⇑(directSumRight' R S M₁' M₂) = directSumRight R M₁' M₂ :=
+  rfl
+
 end TensorProduct
 
 end Ring

Mathlib/LinearAlgebra/TensorProduct/Tower.lean

@@ -643,6 +643,14 @@ lemma baseChange_mul (f g : Module.End R M) :
 
 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
+
+theorem _root_.LinearEquiv.baseChange_tmul (e : M ≃ₗ[R] N) (a : A) (m : M) :
+    LinearEquiv.baseChange R A M N e (a ⊗ₜ[R] m) = a ⊗ₜ e m :=
+  rfl
+
 /-- `baseChange` as a linear map.
 
 When `M = N`, this is true more strongly as `Module.End.baseChangeHom`. -/
@@ -661,13 +669,9 @@ lemma baseChange_pow (f : Module.End R M) (n : ℕ) :
     (f ^ n).baseChange A = f.baseChange A ^ n :=
   map_pow (Module.End.baseChangeHom _ _ _) f 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
-
 @[simp]
 theorem _root_.LinearEquiv.coe_baseChange (e : M ≃ₗ[R] N) :
-    (e.baseChange R A M N : (A ⊗[R] M →ₗ[A] A ⊗[R] N)) = e.toLinearMap.baseChange A :=
+    (e.baseChange R A M N : (A ⊗[R] M →ₗ[A] A ⊗[R] N)) = LinearMap.baseChange A e :=
   rfl
 
 @[simp]

Mathlib/RingTheory/IsTensorProduct.lean

@@ -263,9 +263,11 @@ noncomputable nonrec def IsBaseChange.equiv : S ⊗[R] M ≃ₗ[S] N :=
       · intro x y hx hy
         rw [map_add, smul_add, map_add, smul_add, hx, hy] }
 
+@[simp]
 theorem IsBaseChange.equiv_tmul (s : S) (m : M) : h.equiv (s ⊗ₜ m) = s • f m :=
   rfl
 
+@[simp]
 theorem IsBaseChange.equiv_symm_apply (m : M) : h.equiv.symm (f m) = 1 ⊗ₜ m := by
   rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_smul]
 

Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2025 Antoine Chambert-Loir. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Loir
+-/
+module
+
+public import Mathlib.RingTheory.TensorProduct.IsBaseChangePi
+public import Mathlib.LinearAlgebra.FreeModule.Basic
+
+/-! # Base change of a free module
+
+* `IsBaseChange.basis` : the natural basis of the base change of a module with a basis
+
+* `IsBaseChange.free` : a base change of a free module is free.
+
+-/
+
+@[expose] public section
+
+namespace IsBaseChange
+
+variable {R : Type*} [CommSemiring R]
+    {S : Type*} [CommSemiring S] [Algebra R S]
+    {V : Type*} [AddCommMonoid V] [Module R V]
+    {W : Type*} [AddCommMonoid W] [Module R W] [Module S W] [IsScalarTower R S W]
+    {ι : Type*} [DecidableEq ι]
+    {ε : V →ₗ[R] W}
+
+variable (b : Module.Basis ι R V) (ibc : IsBaseChange S ε)
+
+/-- The basis of a module deduced by base change from a free module with a basis. -/
+noncomputable def basis :
+    Module.Basis ι S W where
+  repr := (ibc.equiv.symm.trans (b.repr.baseChange R S _ _)).trans
+      (finsuppPow ι (linearMap R S)).equiv
+
+theorem basis_apply (i) : ibc.basis b i = ε (b i) := by
+  simp [basis]
+  simp [LinearEquiv.baseChange]
+  generalize_proofs _ _ _ _ ibcRA
+  have : ibcRA.equiv.symm (Finsupp.single i 1) = 1 ⊗ₜ (Finsupp.single i 1) := by
+    simp [LinearEquiv.symm_apply_eq, IsBaseChange.equiv_tmul]
+  simp [this, IsBaseChange.equiv_tmul]
+
+theorem basis_repr_comp_apply (v i) :
+    (ibc.basis b).repr (ε v) i = algebraMap R S (b.repr v i):= by
+  conv_lhs => rw [← b.linearCombination_repr v, Finsupp.linearCombination_apply,
+    map_finsuppSum, map_finsuppSum]
+  simp only [map_smul, Finsupp.sum_apply]
+  rw [Finsupp.sum_eq_single i]
+  · rw [← IsScalarTower.algebraMap_smul S (b.repr v i) (ε (b i)),
+      map_smul, ← ibc.basis_apply]
+    simp [Finsupp.single_eq_same, Algebra.algebraMap_eq_smul_one]
+  · intro i' _ h
+    rw [← IsScalarTower.algebraMap_smul S (b.repr v i') (ε (b i')), map_smul,
+      ← ibc.basis_apply]
+    simp [Finsupp.single_eq_of_ne (Ne.symm h)]
+  · simp
+
+theorem basis_repr_comp (v : V) :
+    (ibc.basis b).repr (ε v) =
+      Finsupp.mapRange.linearMap (Algebra.linearMap R S) (b.repr v) := by
+  ext i
+  simp [basis_repr_comp_apply]
+
+variable [Module.Free R V]
+
+include ibc in
+theorem free : Module.Free S W :=
+  Module.Free.of_basis (ibc.basis (Module.Free.chooseBasis R V))
+
+end IsBaseChange