fgSystem — Mathlib

English

Define the directed system whose objects are finitely generated submodules N of M, with arrows given by inclusion whenever one submodule is contained in another.

Русский

Определим направленную систему, где объекты — это сколь угодно конечные подмодули N ⊆ M, а стрелки — включения, если один подмодуль содержится в другом.

LaTeX

$$$\\mathrm{fgSystem}(N_1,N_2) = \\text{incl}_{N_1 \\hookrightarrow N_2}$ for $N_1 \\le N_2$.$$

Lean4

/-- The directed system of finitely generated submodules of a module. -/
def fgSystem (N₁ N₂ : { N : Submodule R M // N.FG }) (le : N₁ ≤ N₂) : N₁ →ₗ[R] N₂ :=
  Submodule.inclusion le

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