English
For a group G with WellFoundedLT on Subgroups, G is solvable iff every nontrivial subgroup H satisfies its commutator bracket [H,H] is strictly smaller than H.
Русский
Для группы G с хорошо основанной линейной топологией подгрупп G ε G, G разрешима тогда и только тогда, когда для каждой не нулевой подгруппы H выполняется, что [H,H] < H.
LaTeX
$$IsSolvable G ⇔ ∀ H, H ≠ ⊥ → ([H,H], H)$$
Lean4
theorem isSolvable_iff_commutator_lt [WellFoundedLT (Subgroup G)] :
IsSolvable G ↔ ∀ H : Subgroup G, H ≠ ⊥ → ⁅H, H⁆ < H :=
by
refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩
suffices h : IsSolvable (⊤ : Subgroup G) from solvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))
refine WellFoundedLT.induction (C := fun (H : Subgroup G) ↦ IsSolvable H) ⊤ fun H hH ↦ ?_
rcases eq_or_ne H ⊥ with rfl | h'
· infer_instance
· obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')
use n + 1
rw [← (map_injective (subtype_injective _)).eq_iff, Subgroup.map_bot] at hn ⊢
rw [← hn]
clear hn
induction n with
| zero =>
rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator, ← MonoidHom.range_eq_map, ←
MonoidHom.range_eq_map, range_subtype, range_subtype]
| succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
