isFiniteLength_iff_exists_compositionSeries

English

As before, IsFiniteLength(R,M) is equivalent to the existence of a composition series of Submodules of M with head ⊥ and last ⊤.

Русский

Как и прежде, конечная длина модуля эквивалентна существованию композиционной серии подсистем M с головой ⊥ и последним ⊤.

LaTeX

$$$\\operatorname{IsFiniteLength} R M \\iff \\exists s : CompositionSeries (Submodule R M), s.head = \\bot \\land s.last = \\top$$$

Lean4

theorem isFiniteLength_iff_exists_compositionSeries :
    IsFiniteLength R M ↔ ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ :=
  ⟨fun h ↦
    have ⟨_, _⟩ := isFiniteLength_iff_isNoetherian_isArtinian.mp h
    exists_compositionSeries_of_isNoetherian_isArtinian R M,
    isFiniteLength_of_exists_compositionSeries⟩

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