Tensor product with direct limit of finitely generated submodules

we show that if M and P are arbitrary modules and N is a finitely generated submodule of a module P, then two elements of N ⊗ M have the same image in P ⊗ M if and only if they already have the same image in N' ⊗ M for some finitely generated submodule N' ≥ N. This is the theorem Submodule.FG.exists_rTensor_fg_inclusion_eq. The key facts used are that every module is the direct limit of its finitely generated submodules and that tensor product preserves colimits.

theorem Submodule.FG.exists_rTensor_fg_inclusion_eq {R : Type u_1} {M : Type u_2} {P : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {N : Submodule R P} (hN : N.FG) {x y : TensorProduct R (↥N) M} (eq : (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y) : ∃ (N' : Submodule R P), N'.FG ∧ ∃ (h : N ≤ N'), (LinearMap.rTensor M (Submodule.inclusion h)) x = (LinearMap.rTensor M (Submodule.inclusion h)) y