directedSystem — Mathlib

English

The system of modules P ⊗ N, where P ranges FG-submodules of M, forms a directed system with transition maps rTensor N (Submodule.inclusion).

Русский

Система модулей P ⊗ N, где P пробегает FG-подмодули M, образует направленную систему переходными отображениями rTensor N (Submodule.inclusion).

LaTeX

$$$\\text{DirectedSystem}(\\{ P\\mid P.FG \\}, P\\otimes_R N, P≤Q \\mapsto \\text{inclusion}(P≤Q)\\,\\text{rTensor }N).$$$

Lean4

/-- When `P` ranges over finitely generated submodules of `M`,
  the modules of the form `P ⊗[R] N` form a directed system. -/
theorem directedSystem :
    DirectedSystem (ι := { P : Submodule R M // P.FG }) (fun P ↦ P.val ⊗[R] N)
      (fun ⦃_ _⦄ h ↦ rTensor N (Submodule.inclusion h)) :=
  Submodule.FG.directedSystem.rTensor R N

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