fg_of_submodule_fg — Mathlib

English

If the top submodule is finitely generated, then the top subalgebra is finitely generated.

Русский

Если верхний подмодуль FG, то и верхняя подалгебра FG.

LaTeX

$$$ (\\top : Submodule\\ R A).FG \\rightarrow (\\top : Subalgebra\\ R A).FG $$$

Lean4

theorem fg_of_submodule_fg (h : (⊤ : Submodule R A).FG) : (⊤ : Subalgebra R A).FG :=
  let ⟨s, hs⟩ := h
  ⟨s,
    toSubmodule.injective <| by
      rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
      exact Algebra.subset_adjoin⟩

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