Polycyclic.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Polycyclic and virtually polycyclic groups

We use the existing concrete cyclic subnormal series, including normality and cyclicity of each quotient. Neither polycyclicity nor virtual polycyclicity is an unspecified property parameter.

def OAI.PolycyclicRecognition.IsPolycyclic line 22
Source documentation
A polycyclic group has a finite subnormal series from the trivial subgroup to the whole group with cyclic factors.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:61 (same declaration text).
```
def IsPolycyclic : Prop :=
…
```
def OAI.PolycyclicRecognition.IsVirtuallyPolycyclic line 26
Source documentation
A virtually polycyclic group contains a polycyclic subgroup of finite index.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:65 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.IsVirtuallyPolycyclic@path.
```
def IsVirtuallyPolycyclic : Prop :=
…
```
theorem OAI.PolycyclicRecognition.isPolycyclic_of_subsingleton line 32
Source documentation
The length-zero series proves polycyclicity of the trivial group.
```
theorem isPolycyclic_of_subsingleton [Subsingleton G] : IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.IsPolycyclic.of_surjective line 39
Source documentation
Polycyclicity descends to a surjective image by mapping a cyclic series.
```
theorem IsPolycyclic.of_surjective (hG : IsPolycyclic G)
    (f : G →* H) (hf : Function.Surjective f) : IsPolycyclic H := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.IsPolycyclic.of_injective line 48
Source documentation
Subgroups of polycyclic groups are polycyclic, by pulling back the cyclic series.
```
theorem IsPolycyclic.of_injective (hG : IsPolycyclic G)
    (f : H →* G) (hf : Function.Injective f) : IsPolycyclic H := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.isPolycyclic_equiv line 58
Source documentation
This formulation is invariant under group isomorphisms.
```
theorem isPolycyclic_equiv (e : G ≃* H) : IsPolycyclic G ↔ IsPolycyclic H :=
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.IsPolycyclic.isVirtuallyPolycyclic line 63
Source documentation
A polycyclic group is virtually polycyclic, using the whole group.
```
theorem IsPolycyclic.isVirtuallyPolycyclic (hG : IsPolycyclic G) :
    IsVirtuallyPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.isVirtuallyPolycyclic_of_finite line 70
Source documentation
Every finite group is virtually polycyclic, via its trivial subgroup. The ambient finite group itself need not be solvable.
```
theorem isVirtuallyPolycyclic_of_finite [Finite G] : IsVirtuallyPolycyclic G :=
…
```
theorem OAI.PolycyclicRecognition.IsVirtuallyPolycyclic.of_injective line 74
Source documentation
A subgroup of a virtually polycyclic group is virtually polycyclic.
```
theorem IsVirtuallyPolycyclic.of_injective (hG : IsVirtuallyPolycyclic G)
    (f : H →* G) (hf : Function.Injective f) : IsVirtuallyPolycyclic H := by
…
```