directLimit_apply' — Mathlib

English

There is a canonical linear equivalence between the direct limit on the left and the tensor product M ⊗_R N, compatible with inclusions.

Русский

Существует каноническое линейное эквивалентное отображение между прямым пределом слева и M ⊗_R N, совместимое с инклюзиями.

LaTeX

$$$\\text{directLimit}(R,M,N) \\cong_ℓ M \\otimes_R N.$$$

Lean4

theorem directLimit_apply' [DecidableEq { Q : Submodule R N // Q.FG }] (Q : Submodule R N) (hQ : Q.FG) (u : M ⊗[R] Q) :
    (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 ↦ lTensor M (inclusion hPQ)) ⟨Q, hQ⟩)
          u) =
      (lTensor M (Submodule.subtype Q)) u :=
  Submodule.FG.lTensor.directLimit_apply R M N ⟨Q, hQ⟩ u

Похожие утверждения