isNoetherian_quotient — Mathlib

English

If A is a module over a ring R and N is a submodule, and M is Noetherian, then the quotient M/N is Noetherian.

Русский

Если M — модуль над кольцом R и N — подмодуль, и M является Noetherian, то фактор-модуль M/N также Noetherian.

LaTeX

$$$\forall N \le M,\ [IsNoetherian\ R\ M] \Rightarrow IsNoetherian R (M/N)$$$

Lean4

instance isNoetherian_quotient {A M : Type*} [Ring A] [AddCommGroup M] [SMul R A] [Module R M] [Module A M]
    [IsScalarTower R A M] (N : Submodule A M) [IsNoetherian R M] : IsNoetherian R (M ⧸ N) :=
  isNoetherian_of_surjective M ((Submodule.mkQ N).restrictScalars R) <| LinearMap.range_eq_top.mpr N.mkQ_surjective

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