English
If s is a composition series with head ⊥ and last ⊤, then its length equals the module length: s.length = Module.length R M.
Русский
Если s — композиционная серия с head = ⊥ и last = ⊤, то её длина равна длине модуля: s.length = Module.length R M.
LaTeX
$$For a composition series s with head s.head = ⊥ and last s.last = ⊤, we have s.length = Module.length R M.$$
Lean4
theorem length_compositionSeries (s : CompositionSeries (Submodule R M)) (h₁ : s.head = ⊥) (h₂ : s.last = ⊤) :
s.length = Module.length R M :=
by
have H := isFiniteLength_of_exists_compositionSeries ⟨s, h₁, h₂⟩
have := (isFiniteLength_iff_isNoetherian_isArtinian.mp H).1
have := (isFiniteLength_iff_isNoetherian_isArtinian.mp H).2
rw [← WithBot.coe_inj, Module.coe_length]
apply le_antisymm
· exact (Order.LTSeries.length_le_krullDim <| s.map ⟨id, fun h ↦ h.1⟩)
· rw [Order.krullDim, iSup_le_iff]
intro t
refine WithBot.coe_le_coe.mpr ?_
obtain ⟨t', i, hi, ht₁, ht₂⟩ := t.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot
have := (s.jordan_holder t' (h₁.trans ht₁.symm) (h₂.trans ht₂.symm)).choose
have h : t.length ≤ t'.length := by simpa using Fintype.card_le_of_embedding i
have h' : t'.length = s.length := by simpa using Fintype.card_congr this.symm
simpa using h.trans h'.le
