English
For a Lie ideal I and natural k, the length equals k+1 exactly when the k-th derived series of I is abelian and nonzero.
Русский
Для идеала Ли I и натурального k длина равна k+1 тогда и только тогда, когда k-я производная серия I абелева и не нулевая.
LaTeX
$$$\mathrm{derivedLengthOfIdeal}(R,L,I) = k+1 \;\Longleftrightarrow\; \big( \mathrm{IsLieAbelian}(\mathrm{derivedSeriesOfIdeal}(R,L,k,I)) \land \mathrm{derivedSeriesOfIdeal}(R,L,k,I) \neq \perp \big).$$$
Lean4
theorem derivedSeries_of_derivedLength_succ (I : LieIdeal R L) (k : ℕ) :
derivedLengthOfIdeal R L I = k + 1 ↔
IsLieAbelian (derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥ :=
by
rw [abelian_iff_derived_succ_eq_bot]
let s := {k | derivedSeriesOfIdeal R L k I = ⊥}
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s :=
by
intro k₁ k₂ h₁₂ h₁
suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
change derivedSeriesOfIdeal R L k₁ I = ⊥ at h₁; rw [← h₁]
exact derivedSeriesOfIdeal_antitone I h₁₂
exact Nat.sInf_upward_closed_eq_succ_iff hs k
