English
If f: G →* G' is injective and G' is solvable, then G is solvable.
Русский
Если гомоморфизм f: G →* G' инъективен и G' разрешима, то G разрешимо.
LaTeX
$$IsSolvable G$$
Lean4
theorem solvable_of_ker_le_range {G' G'' : Type*} [Group G'] [Group G''] (f : G' →* G) (g : G →* G'')
(hfg : g.ker ≤ f.range) [hG' : IsSolvable G'] [hG'' : IsSolvable G''] : IsSolvable G :=
by
obtain ⟨n, hn⟩ := id hG''
obtain ⟨m, hm⟩ := id hG'
refine ⟨⟨n + m, le_bot_iff.mp (Subgroup.map_bot f ▸ hm ▸ ?_)⟩⟩
clear hm
induction m with
| zero =>
exact
f.range_eq_map ▸
((derivedSeries G n).map_eq_bot_iff.mp
(le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans
hfg
| succ m hm => exact commutator_le_map_commutator hm hm
