S-isomorphism between colim (M_i ⊗ S) and (colim M_i) ⊗ S

Stream: mathlib4

[Liran Shaul]

Hi everyone,

I am trying to construct an $S$-linear isomorphism between the tensor product of a direct limit and the direct limit of the tensored modules.

Specifically, given:

• A directed system of $R$-modules $M_i$ with transition maps $f_{ij} : M_i \to M_j$.

• A commutative ring map $R \to S$.

• The induced system of $S$-modules $M_i \otimes_R S$ with transition maps $f_{ij} \otimes \text{id}_S$.

I have an $R$-linear isomorphism:

iso_lim : (Module.DirectLimit M f) ⊗[R] S ≃ₗ[R] Module.DirectLimit (fun i ↦ M i ⊗[R] S) (fun i j h ↦ lTensor S (f h))

The Problem:

I need this to be an $S$-linear isomorphism (≃ₗ[S]) and I need it to target a slightly different definition of the transition maps:

f_tensor : i ≤ j → M i ⊗ S →ₗ[S] M j ⊗ S

defined via TensorProduct.AlgebraTensorModule.map.

Even though the transition maps are extensionally equal, I am hitting a wall because:

1. Module.DirectLimit.lift is producing $R$-linear maps when I need $S$-linear maps.

2. The typeclass engine is getting stuck on metavariables when I try to use LinearEquiv.ofLinear to upgrade the $R$-equivalence, likely because the Module S instance on the DirectLimit depends on the specific form of the transition maps.

How can I best define this $S$-isomorphism such that it respects the $S$-module structure on both sides without falling into definitional hell regarding the transition maps?

-- Transition maps in the goal
f_tensor : (i j : ι) → i ≤ j → S ⊗[R] G i →ₗ[S] S ⊗[R] G j := fun i j h ↦ TensorProduct.AlgebraTensorModule.map LinearMap.id (f h)
-- The S-module instance I am using
instance : Module S (Module.DirectLimit (fun i ↦ S ⊗[R] G i) f_tensor) := Module.DirectLimit.module _ f_tensor

[Kevin Buzzard]

I'm not at a computer right now but we did a bunch of relevant material in FLT (edit: but probably not exactly what you need).