PolycyclicDualityComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The algebraic Poincaré-duality comparison group

Only two standard published consequences are needed here:

D. J. S. Robinson, A Course in the Theory of Groups, second edition, GTM 80, Springer (1996), Theorem 5.4.15(i), p.153: every polycyclic group has a finite-index poly-infinite-cyclic subgroup. We use only its torsion-free consequence, not normality or a chosen infinite-cyclic series.
R. Bieri, Homological Dimension of Discrete Groups, second edition (1981), Theorems 9.9 and 9.10, and their explicit consequence on p.176: every torsion-free polycyclic group is an integral Poincaré-duality group.

These are explicit conditional inputs. The resulting recognition theorem retains elementary amenability as a hypothesis.

def OAI.PolycyclicRecognition.HasNoNontrivialTorsion line 25
Source documentation
Group-theoretic torsion freeness. This only excludes nonidentity finite-order elements; it does not impose the unique-root property on a noncommutative group.
```
def HasNoNontrivialTorsion (P : Type) [Group P] : Prop :=
…
```
def OAI.PolycyclicRecognition.PolycyclicTorsionFreeIndexInput line 29
Source documentation
The torsion-free consequence of Robinson 5.4.15(i).
```
def PolycyclicTorsionFreeIndexInput : Prop :=
…
```
def OAI.PolycyclicRecognition.BieriPolycyclicDualityInput line 34
Source documentation
The precise polycyclic specialization of Bieri's duality theorems.
```
def BieriPolycyclicDualityInput : Prop :=
…
```

theorem OAI.PolycyclicRecognition.exists_coarse_poincareDuality_comparison line 40

Source documentation

A virtual-polycyclic comparison group supplies an actual finitely generated integral duality group in the same coarse equivalence class.

theorem exists_coarse_poincareDuality_comparison
    (tf : PolycyclicTorsionFreeIndexInput) (pd : BieriPolycyclicDualityInput)
    (P H : Type) [Group P] [Group H] [Group.FG P]
    (hP : IsVirtuallyPolycyclic P) (e : GroupCoarseEquivalence P H) :
    ∃ (K : Subgroup P) (Γ : Subgroup K),
      K.FiniteIndex ∧ Γ.FiniteIndex ∧ Group.FG Γ ∧
      Nonempty (GroupCoarseEquivalence Γ H) ∧
      ∃ n : ℕ, IsIntegralPoincareDualityGroup Γ n := by
…

Mentions: OAI.PolycyclicRecognition.PolycyclicTorsionFreeIndexInput, OAI.PolycyclicRecognition.BieriPolycyclicDualityInput, OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_elementaryAmenable_coarse_virtualPolycyclic line 61
Source documentation
An elementary amenable group coarsely equivalent to a virtually polycyclic group is virtually polycyclic, given the finiteness and duality inputs.
```
theorem virtuallyPolycyclic_of_elementaryAmenable_coarse_virtualPolycyclic
    (tf : PolycyclicTorsionFreeIndexInput) (pd : BieriPolycyclicDualityInput)
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    (P H : Type) [Group P] [Group H] [Group.FG P] [Group.FG H]
    (hP : IsVirtuallyPolycyclic P) (e : GroupCoarseEquivalence P H)
    (hEA : IsElementaryAmenable H) : IsVirtuallyPolycyclic H := by
…
```
Mentions: OAI.PolycyclicRecognition.PolycyclicTorsionFreeIndexInput, OAI.PolycyclicRecognition.BieriPolycyclicDualityInput, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.IsElementaryAmenable