coeSubmodule_fg — Mathlib

English

For any ideal I, the finitely generated status is preserved under coeSubmodule: (coeSubmodule(S,I)).FG ⇔ I.FG, provided the appropriate injection condition.

Русский

Для идеала I условие «конечнопорождённость» сохраняется через coeSubmodule: (coeSubmodule(S,I)).FG ⇔ I.FG при заданной инъекции.

LaTeX

$$coeSubmodule_fg : (coeSubmodule S I).FG ↔ I.FG$$

Lean4

theorem coeSubmodule_fg (hS : Function.Injective (algebraMap R S)) (I : Ideal R) :
    Submodule.FG (coeSubmodule S I) ↔ Submodule.FG I :=
  ⟨Submodule.fg_of_fg_map_injective _ hS, Submodule.FG.map _⟩

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