NilpotentAbelianFiniteness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite generation detected on abelian subgroups of nilpotent groups

In class two, commutators with finitely many generators of a maximal abelian normal subgroup embed the quotient into a finite power of the center. Induction through the center quotient reduces the general nilpotent case to this one.

theorem OAI.PolycyclicRecognition.isPolycyclic_of_central_commutators line 24
Source documentation
The class-two case uses only abelian subgroups, their finite generating sets, and the central commutator pairing.
```
theorem isPolycyclic_of_central_commutators
    (hc : ∀ x y : G, ⁅x, y⁆ ∈ Subgroup.center G)
    (hfg : ∀ A : Subgroup G, IsMulCommutative A → Group.FG A) : IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic

theorem OAI.PolycyclicRecognition.abelian_subgroups_fg_of_injective line 94

Source documentation

The hypothesis that abelian subgroups are finitely generated passes to an injectively represented subgroup.

theorem abelian_subgroups_fg_of_injective
    (hfg : ∀ A : Subgroup G, IsMulCommutative A → Group.FG A)
    {H : Type*} [Group H] (f : H →* G) (hf : Function.Injective f) :
    ∀ A : Subgroup H, IsMulCommutative A → Group.FG A := by
…

theorem OAI.PolycyclicRecognition.isPolycyclic_of_nilpotent_abelian_subgroups_fg line 106
Source documentation
In a nilpotent group, finite generation of every abelian subgroup suffices for polycyclicity of the whole group.
```
theorem isPolycyclic_of_nilpotent_abelian_subgroups_fg [Group.IsNilpotent G]
    (hfg : ∀ A : Subgroup G, IsMulCommutative A → Group.FG A) : IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic