English
An alternative version of the DirectLimit Apply lemma, using a particular FG P and hP; the equality is preserved under the reindexed representation.
Русский
Альтернативная версия леммы DirectLimit Apply, использующая конкретный FG P и hP; равенство сохраняется при перенумерации.
LaTeX
$$$\\text{DirectLimit Apply' }(R,M,N)\\; (P,hP,u) : \\text{равно } \\text{DirectLimit Apply}(R,M,N)\\; P\\; u.$$$
Lean4
/-- An alternative version to `Submodule.FG.rTensor.directLimit_apply`. -/
theorem directLimit_apply' [DecidableEq { P : Submodule R M // P.FG }] {P : Submodule R M} (hP : Submodule.FG P)
(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 ↦ rTensor N (Submodule.inclusion h)) ⟨P, hP⟩)
u) =
(rTensor N (Submodule.subtype P)) u :=
by apply Submodule.FG.rTensor.directLimit_apply
