isNoetherian_of_tower — Mathlib

English

If M is Noetherian as an R-module and S acts on M through a scalar tower R → S → End(M), then M is Noetherian as an S-module.

Русский

Если M Ноетеров как R-модуль и действует через цилиндр-слой R → S → End(M), то M ноетеров как S-модуль.

LaTeX

$$$IsNoetherian(S,M)$ from $IsNoetherian(R,M)$ and IsScalarTower(R,S,M)$$

Lean4

/-- If `M / S / R` is a scalar tower, and `M / R` is Noetherian, then `M / S` is
also Noetherian. -/
theorem isNoetherian_of_tower (R) {S M} [Semiring R] [Semiring S] [AddCommMonoid M] [SMul R S] [Module S M] [Module R M]
    [IsScalarTower R S M] (h : IsNoetherian R M) : IsNoetherian S M :=
  isNoetherian_mk ⟨(Submodule.restrictScalarsEmbedding R S M).dual.wellFounded h.wf⟩

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