English
A module M has finite length if and only if there exists a composition series of Submodules of M with head ⊥ and last ⊤.
Русский
Модуль M имеет конечную длину тогда и только тогда, когда существует композиционная серия подсистем M с головой ⊥ и последним ⊤.
LaTeX
$$$\\operatorname{IsFiniteLength} R M \\iff \\exists s : CompositionSeries (Submodule R M), s.head = ⊥ \\land s.last = ⊤$$$
Lean4
theorem isFiniteLength_of_exists_compositionSeries
(h : ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤) : IsFiniteLength R M :=
Submodule.topEquiv.isFiniteLength <| by
obtain ⟨s, s_head, s_last⟩ := h
rw [← s_last]
suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
intro i
induction i using Fin.induction with
| zero => change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
| succ i ih =>
let cov := s.step i
have := (covBy_iff_quot_is_simple cov.le).mp cov
have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective _ (Submodule.injective_subtype _)
rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
exact .of_simple_quotient (this.symm.isFiniteLength ih)
