Refactor Submodule.baseChange and LinearMap.baseChange

Stream: mathlib4

[Kenny Lau]

Submodule.baseChange:

def baseChange (p : Submodule R M) : Submodule A (A ⊗[R] M) :=
  span A <| p.map (TensorProduct.mk R A M 1)

LinearMap.baseChange:

def baseChange (f : M →ₗ[R] N) : A ⊗[R] M →ₗ[A] A ⊗[R] N :=
  AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) f

lTensor.equiv

noncomputable def lTensor.equiv (hfg : Exact f g) (hg : Function.Surjective g) :
    ((Q ⊗[R] N) ⧸ (LinearMap.range (lTensor Q f))) ≃ₗ[R] (Q ⊗[R] P) :=
  lTensor.linearEquiv_of_rightInverse Q hfg (Function.rightInverse_surjInv hg)

Basically, Submodule.baseChange is currently not defeq to a form that is easily usable in lTensor.equiv or related lemmas about right-exactness of tensor.

I propose to change the definition of Submodule.baseChange to LinearMap.range (S.subtype.baseChange A).

Searching on Loogle Submodule.baseChange and subsequently LieSubmodule.baseChange show 8 and 11 hits respectively, which shows that Submodule.baseChange is seldom used, so this change will likely not to have a large impact.

@Andrew Yang What are your opinions?

[Andrew Yang]

The change makes sense to me.

[Kenny Lau]

#26019