isArtinian_of_tower — Mathlib

English

If M is Artinian over R and there is a scalar tower R → S → M, then M is Artinian over S.

Русский

Если M — артинановый модуль над R и существует каскад скаляров R → S → M, тогда M артинанов относительно S.

LaTeX

$$$ IsArtinian\\; R\\; M \\Rightarrow IsArtinian\\; S\\; M. $$$

Lean4

/-- If `M / S / R` is a scalar tower, and `M / R` is Artinian, then `M / S` is also Artinian. -/
theorem isArtinian_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 : IsArtinian R M) : IsArtinian S M :=
  ⟨(Submodule.restrictScalarsEmbedding R S M).wellFounded h.wf⟩
    -- See `Mathlib/RingTheory/Artinian/Ring.lean`

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