isNoetherian_iff_submodule_quotient

English

For any submodule S of P, P is Noetherian if and only if both S is Noetherian and P/S is Noetherian.

Русский

Для любого подмодуля S P верно: P Noetherian тогда и только тогда, когда S Noetherian и P/S Noetherian.

LaTeX

$$$IsNoetherian R P \iff IsNoetherian R S \land IsNoetherian R (P/S)$$$

Lean4

theorem isNoetherian_iff_submodule_quotient (S : Submodule R P) :
    IsNoetherian R P ↔ IsNoetherian R S ∧ IsNoetherian R (P ⧸ S) :=
  by
  refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
  apply isNoetherian_of_range_eq_ker S.subtype S.mkQ
  rw [Submodule.ker_mkQ, Submodule.range_subtype]

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