NilpotentRecognition.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent comparison branch

A coarse embedding into a simply connected nilpotent Lie group gives polynomial intrinsic word growth, by the proved nilpotent chain-packing estimate. The final passage to virtual nilpotence uses exactly Gromov's published polynomial-growth theorem. This settles the nilpotent branch; the general solvable height argument remains separate.

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_coarseEmbedding_nilpotent_lieGroup line 32

Source documentation

The nilpotent branch of recognition, with only the precise published exponential and polynomial-growth inputs. Surjectivity of the coarse map is not needed for this branch.

theorem virtuallyPolycyclic_of_coarseEmbedding_nilpotent_lieGroup
    (dynkin : NilpotentDynkinExpansionInput E G)
    (haarInput : NilpotentExponentialHaarInput E G)
    (gromov : GromovPolynomialGrowthInput H)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (f : H → G) (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    {K C K' C' : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hK' : 0 ≤ K')
    (hupper : ∀ x y, dist (f x) (f y) ≤ K * dist x y + C)
    (hlower : ∀ x y, dist x y ≤ K' * dist (f x) (f y) + C') :
    IsVirtuallyPolycyclic H := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.GromovPolynomialGrowthInput

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_coarseEmbedding_height_zero line 53

Source documentation

The canonical zero-height branch follows from the triangular adjoint matrices and Engel's theorem; nilpotence is not an additional premise.

theorem virtuallyPolycyclic_of_coarseEmbedding_height_zero
    (dynkin : NilpotentDynkinExpansionInput E G)
    (haarInput : NilpotentExponentialHaarInput E G)
    (gromov : GromovPolynomialGrowthInput H)
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    [Subsingleton (HeightSpace T.character)]
    (f : H → G) (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    {K C K' C' : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hK' : 0 ≤ K')
    (hupper : ∀ x y, dist (f x) (f y) ≤ K * dist x y + C)
    (hlower : ∀ x y, dist x y ≤ K' * dist (f x) (f y) + C') :
    IsVirtuallyPolycyclic H :=
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace