ElementaryAmenable.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Elementary amenability of the height extension

We use the closure definition: finite and abelian groups, subgroups, quotients, extensions, and directed unions. For the last operation it suffices to use the directed union of the finitely generated subgroups. This formulation is exactly what is needed when the corrected height kernel is locally virtually nilpotent. In particular, no finite generation of that kernel is imposed.

inductive OAI.PolycyclicRecognition.IsElementaryAmenable line 21
Source documentation
The elementary amenable class, with directed-union closure expressed by the canonical directed family of all finitely generated subgroups.
```
inductive IsElementaryAmenable : (G : Type u) → [Group G] → Prop where
…
```
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_derivedSeries_eq_bot line 41
Source documentation
A finite derived series places a group in the elementary amenable class.
```
theorem elementaryAmenable_of_derivedSeries_eq_bot (n : ℕ) :
    ∀ (G : Type u) [Group G], derivedSeries G n = ⊥ → IsElementaryAmenable G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsElementaryAmenable
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_solvable line 65
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_finiteIndex line 72
Source documentation
Elementary amenability passes from a finite-index subgroup to its ambient group, using the normal core without assuming the original subgroup normal.
```
theorem elementaryAmenable_of_finiteIndex {G : Type u} [Group G]
    (H : Subgroup G) [H.FiniteIndex] (hH : IsElementaryAmenable H) :
    IsElementaryAmenable G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsElementaryAmenable
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_finiteIndex_solvable line 82
Source documentation
A finite extension of a solvable subgroup is elementary amenable. Normality is obtained by taking the finite-index normal core.
```
theorem elementaryAmenable_of_finiteIndex_solvable {G : Type u} [Group G]
    (H : Subgroup G) [H.FiniteIndex] [Group.IsSolvable H] : IsElementaryAmenable G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsElementaryAmenable
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_virtuallyNilpotent line 90
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_locallyVirtuallyNilpotent line 99
Source documentation
Local virtual nilpotence is sufficient even for an infinitely generated group, as occurs for a nondiscrete height homomorphism.
```
theorem elementaryAmenable_of_locallyVirtuallyNilpotent {G : Type u} [Group G]
    (hG : ∀ J : Subgroup G, Group.FG J → Group.IsVirtuallyNilpotent J) :
    IsElementaryAmenable G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsElementaryAmenable
theorem OAI.PolycyclicRecognition.elementaryAmenable_of_height_kernel line 106
Source documentation
An abelian height quotient and a locally virtually nilpotent kernel give elementary amenability of the domain.
```
theorem elementaryAmenable_of_height_kernel {G A : Type u} [Group G] [CommGroup A]
    (τ : G →* A)
    (hker : ∀ J : Subgroup τ.ker, Group.FG J → Group.IsVirtuallyNilpotent J) :
    IsElementaryAmenable G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsElementaryAmenable