exists_compositionSeries_of_isNoetherian_isArtinian

English

If a module M is Noetherian and Artinian, there exists a composition series of Submodules of M whose head is ⊥ and last is ⊤.

Русский

Если модуль M Noetherian и Artinian, существует композиционная серия подсистем Submodule R M с головой ⊥ и последним ⊤.

LaTeX

$$$\\exists s : CompositionSeries (Submodule R M), s.head = \\bot \\land s.last = \\top$$$

Lean4

theorem exists_compositionSeries_of_isNoetherian_isArtinian [IsNoetherian R M] [IsArtinian R M] :
    ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ :=
  by
  obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)
  exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩

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