isArtinian_iff_submodule_quotient

English

Artinian property is equivalent to its submodule and its quotient being Artinian.

Русский

Артинановость равносильна её подмодулю и фактормодулю.

LaTeX

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

Lean4

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

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