OAI/GroupTheory/PolycyclicRecognition/Algebra/RecognitionFromLeafTraces.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_leaf_and_traces line 17

   Source documentation

   The actual transferred maps need not use an inverse normalized at the identity. Its fixed basepoint error is uniformly bounded by the coarse map and height controls. The geometric leaf and trace estimates then supply both finiteness/duality recognition conclusions.

   theorem recognition_and_lattice_of_leaf_and_traces
       (dekimpe : DekimpeLatticeRealizationInput)
       (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
       (liPD : LiDualityInput) (bieri : BieriDualityInput)
       {P J : Type} [Group P] [Group J] [MetricSpace P] [MetricSpace J]
       [IsIsometricSMul P P] [IsIsometricSMul J J] [Group.FG P] [Group.FG J]
       [DiscreteTopology J] [ProperSpace J]
       [MeasurableSpace J] [BorelSpace J] [MeasurableMul J]
       (e : MetricQuasiEquivalence P J) (hP : IsVirtuallyPolycyclic P)
       (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
       {E G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
       [MetricSpace G] [ChartedSpace E G] [Group G] [LieGroup (𝓘(ℝ, E)) ⊤ G]
   …

   Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.MetricQuasiEquivalence