OAI/GroupTheory/PolycyclicRecognition/Geometry/RecognitionInLieModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finiteness and duality in a concrete Lie model

Canonical-height packing, a corrected height estimate and an integral Poincaré-duality comparison imply virtual polycyclicity.

  1. theorem OAI.PolycyclicRecognition.elementaryAmenable_of_corrected_canonical_height line 33

    Source documentation

    Corrected canonical height in the actual Lie group implies elementary amenability, using published realization and Gromov inputs only for packing.

    theorem elementaryAmenable_of_corrected_canonical_height
    (dixmier : DixmierExponentialInput (E := E) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.DixmierExponentialInput

  2. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_corrected_canonical_height line 50

    Source documentation

    The Lie-model growth estimate combines with the finiteness and duality theorems under geometric height and comparison-model hypotheses.

    theorem virtuallyPolycyclic_of_corrected_canonical_height
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    (dixmier : DixmierExponentialInput (E := E) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.DixmierExponentialInput