English
The direct limit of FG-submodules under rTensor with N is canonically identified with the tensor product M ⊗_R N.
Русский
Прямой предел FG-подмодулов с учетом rTensor на N канонически идентифицируется с тензорным произведением M ⊗_R N.
LaTeX
$$$\\text{Submodule.FG.rTensor.directLimit\\,R\\,M\\,N} \\cong_{\\text{linear}} M \\otimes_R N.$$$
Lean4
/-- A tensor product `M ⊗[R] N` is the direct limit of the modules `P ⊗[R] N`,
where `P` ranges over all finitely generated submodules of `M`, as a linear equivalence. -/
noncomputable def directLimit [DecidableEq { P : Submodule R M // P.FG }] :
Module.DirectLimit (R := R) (ι := { P : Submodule R M // P.FG }) (fun P ↦ P.val ⊗[R] N)
(fun ⦃P Q⦄ (h : P ≤ Q) ↦ (Submodule.inclusion h).rTensor N) ≃ₗ[R]
M ⊗[R] N :=
(TensorProduct.directLimitLeft _ N).symm.trans ((Submodule.FG.directLimit R M).rTensor N)
