FiniteKernelSolvable.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing a finite normal kernel from virtual solvability

This is the elementary centralizer step used in §2 of Kropholler–Martínez-Pérez–Nucinkis (2009). It does not assume any finiteness theorem for elementary amenable groups.

theorem OAI.PolycyclicRecognition.conjugation_ker_eq_centralizer line 20
theorem OAI.PolycyclicRecognition.finiteIndex_centralizer_of_finite_normal line 35
theorem OAI.PolycyclicRecognition.exists_finiteIndex_solvable_of_finite_kernel line 43
Source documentation
If the quotient by a finite normal subgroup is virtually solvable, the ambient group is virtually solvable. Intersect the lifted solvable subgroup with the centralizer of the finite kernel; its new kernel is abelian.
```
theorem exists_finiteIndex_solvable_of_finite_kernel [Finite N]
    (hQ : ∃ V : Subgroup (G ⧸ N), V.FiniteIndex ∧ Group.IsSolvable V) :
    ∃ H : Subgroup G, H.FiniteIndex ∧ Group.IsSolvable H := by
…
```