English
The equivalence Submodule.FG.rTensor.directLimit R M N with the left-tensor direct limit is the canonical linear equivalence between the two constructions.
Русский
Эквивалентность между Submodule.FG.rTensor.directLimit и левым пределом тензорного произведения является каноническим линейным эквивалентом между двумя конструкциями.
LaTeX
$$$ Submodule.FG.rTensor.directLimit\\; R\\; M\\; N \\cong_ℓ\\; (TensorProduct.directLimitLeft \\ldots ).$$$
Lean4
/-- A tensor product `M ⊗[R] N` is the direct limit of the modules `M ⊗[R] Q`,
where `Q` ranges over all finitely generated submodules of `N`, as a linear equivalence. -/
noncomputable def directLimit [DecidableEq { Q : Submodule R N // Q.FG }] :
Module.DirectLimit (R := R) (ι := { Q : Submodule R N // Q.FG }) (fun Q ↦ M ⊗[R] Q.val)
(fun _ _ hPQ ↦ (inclusion hPQ).lTensor M) ≃ₗ[R]
M ⊗[R] N :=
(TensorProduct.directLimitRight _ M).symm.trans ((Submodule.FG.directLimit R N).lTensor M)
