English
A symmetrical variant of directLimit_apply expresses that evaluating at a representative yields the same rTensor value as the target.
Русский
Симметричная версия directLimit_apply выражает, что вычисление по представителю даёт тот же результат rTensor, что и цель.
LaTeX
$$$\\text{DirectLimit apply'}(R,M,N)\\; u = \\text{DirectLimit apply}(R,M,N)\\; u.$$$
Lean4
theorem directLimit_apply [DecidableEq { P : Submodule R N // P.FG }] (Q : { Q : Submodule R N // Q.FG })
(u : M ⊗[R] Q.val) :
(Submodule.FG.lTensor.directLimit R M N)
((Module.DirectLimit.of R { Q : Submodule R N // Q.FG } (fun Q ↦ M ⊗[R] Q.val)
(fun _ _ hPQ ↦ (inclusion hPQ).lTensor M) Q)
u) =
(lTensor M (Submodule.subtype Q.val)) u :=
by
suffices
(Submodule.FG.lTensor.directLimit R M N).toLinearMap.comp
(Module.DirectLimit.of R { Q : Submodule R N // Q.FG } (fun Q ↦ M ⊗[R] Q.val)
(fun _ _ hPQ ↦ lTensor M (inclusion hPQ)) Q) =
lTensor M (Submodule.subtype Q.val)
by exact DFunLike.congr_fun this u
ext p n
simp [Submodule.FG.lTensor.directLimit, Submodule.FG.directLimit]
