directedSystem — Mathlib

English

The FG-submodules of M form a directed system under inclusion, whose maps are the inclusions between submodules.

Русский

Подмодули M, обладающие свойством FG, образуют направленную систему относительно включения, переходные отображения — включения между подмодулями.

LaTeX

$$$\\text{DirectedSystem}_{\\iota={P\\subseteq M\\,|\\,P\\text{ FG}}}\\bigl(P\\mapsto P\\bigr)\\text{ with } f(h)=\\iota(h).$$$

Lean4

/-- The directed system of finitely generated submodules of `M` -/
instance directedSystem :
    DirectedSystem (ι := { P : Submodule R M // P.FG }) (F := fun P ↦ P.val) (f := fun ⦃P Q⦄ (h : P ≤ Q) ↦
      Submodule.inclusion h)
    where
  map_self := fun _ _ ↦ rfl
  map_map := fun _ _ _ _ _ _ ↦ rfl

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