GromovInput.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The polynomial-growth input in height-kernel recognition

Published input: M. Gromov, Groups of polynomial growth and expanding maps, Publications Mathématiques de l'IHÉS 53 (1981), 53–78, Main Theorem, p. 54, DOI: 10.1007/BF02698687.

GromovPolynomialGrowthInput J is precisely the implication needed here: a finite symmetric generating set with polynomially bounded intrinsic word balls gives a nilpotent subgroup of finite index. The supporting covering-to-cardinality argument uses concrete finite word balls, with this implication as an explicit hypothesis.

abbrev OAI.PolycyclicRecognition.IsVirtuallyNilpotent line 29
Source documentation
Virtual nilpotency means the existence of a nilpotent subgroup of finite index.
```
abbrev IsVirtuallyNilpotent : Prop := Group.IsVirtuallyNilpotent J
```
def OAI.PolycyclicRecognition.GromovPolynomialGrowthInput line 33
Source documentation
Gromov's Main Theorem (1981, p. 54), specialized to the finite symmetric word-ball formulation used by the height-kernel argument.
```
def GromovPolynomialGrowthInput [DecidableEq J] : Prop :=
…
```

theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_polynomial_cover line 46

Source documentation

Polynomial packing and bounded multiplicity imply virtual nilpotency, conditionally on exactly the stated polynomial-growth input of Gromov. No undistortion condition on J is needed.

theorem virtuallyNilpotent_of_polynomial_cover
    (gromov : GromovPolynomialGrowthInput J) (T : Finset J)
    (hsymmetric : ∀ t ∈ T, t⁻¹ ∈ T)
    (hgenerates : Subgroup.closure (T : Set J) = ⊤)
    (f : J → X) (C b M : ℕ) (centers : ℕ → Finset X)
    (hcenters : ∀ n, (centers n).card ≤ C * (1 + n) ^ b)
    (hcover : ∀ n h, h ∈ wordBall T n → ∃ c ∈ centers n, dist (f h) c ≤ 1)
    (hmultiplicity : ∀ (c : X) (A : Finset J),
      (∀ h ∈ A, dist (f h) c ≤ 1) → A.card ≤ M) :
    IsVirtuallyNilpotent J := by
…

Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.wordBall, OAI.PolycyclicRecognition.IsVirtuallyNilpotent

theorem OAI.PolycyclicRecognition.exists_symmetric_finite_generating_set line 62
Source documentation
Finite generation supplies a finite symmetric generating set by adjoining inverses to any finite generating set.
```
theorem exists_symmetric_finite_generating_set [Group.FG J] :
    ∃ T : Finset J, (∀ t ∈ T, t⁻¹ ∈ T) ∧ Subgroup.closure (T : Set J) = ⊤ := by
…
```

theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_finiteGeneration_polynomial_covers line 80

Source documentation

If every finite symmetric generating set has polynomially many covering balls, finite generation and Gromov's precise input yield virtual nilpotency. The uniform multiplicity hypothesis concerns the actual map f.

theorem virtuallyNilpotent_of_finiteGeneration_polynomial_covers [Group.FG J]
    (gromov : GromovPolynomialGrowthInput J) (f : J → X) (M : ℕ)
    (hmultiplicity : ∀ (c : X) (A : Finset J),
      (∀ h ∈ A, dist (f h) c ≤ 1) → A.card ≤ M)
    (hcovers : ∀ T : Finset J, (∀ t ∈ T, t⁻¹ ∈ T) →
      Subgroup.closure (T : Set J) = ⊤ →
      ∃ (C b : ℕ) (centers : ℕ → Finset X),
        (∀ n, (centers n).card ≤ C * (1 + n) ^ b) ∧
        (∀ n h, h ∈ wordBall T n → ∃ c ∈ centers n, dist (f h) c ≤ 1)) :
    IsVirtuallyNilpotent J := by
…

Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.wordBall, OAI.PolycyclicRecognition.IsVirtuallyNilpotent