English
The canonical map from the direct limit to M ⊗ N acts as the rTensor evaluated on the chosen representative; i.e., it commutes with the limit map on u.
Русский
Каноническое отображение прямого предела в M ⊗ N действует как rTensor на выбранного представителя; тождественно по пределу.
LaTeX
$$$\\bigl( Submodule.FG.rTensor.directLimit R M N \\bigr)\\bigl( \\text{Module.DirectLimit.of}(P, P\\FG, \\ldots)\\; u \\bigr) = rTensor\\;N\\; (Submodule.subtype P) \\; u.$$$
Lean4
theorem directLimit_apply [DecidableEq { P : Submodule R M // P.FG }] {P : { P : Submodule R M // P.FG }}
(u : P ⊗[R] N) :
(Submodule.FG.rTensor.directLimit R M N)
((Module.DirectLimit.of R { P : Submodule R M // P.FG } (fun P ↦ P.val ⊗[R] N)
(fun ⦃_ _⦄ h ↦ (Submodule.inclusion h).rTensor N) P)
u) =
(rTensor N (Submodule.subtype P)) u :=
by
suffices
(Submodule.FG.rTensor.directLimit R M N).toLinearMap.comp
(Module.DirectLimit.of R { P : Submodule R M // P.FG } (fun P ↦ P.val ⊗[R] N)
(fun _ _ hPQ ↦ rTensor N (Submodule.inclusion hPQ)) P) =
rTensor N (Submodule.subtype P.val)
by exact DFunLike.congr_fun this u
ext p n
simp [Submodule.FG.rTensor.directLimit, Submodule.FG.directLimit]
