OAI/GroupTheory/PolycyclicRecognition/Lattices/OriginalLatticeComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.nonempty_original_lattice_comparison line 17

   Source documentation

   The discrete finite-index and lattice comparisons become a metric quasi-equivalence in the chosen ambient metric. The linear-chain condition on the original group makes explicit the word-metric scope.

   theorem nonempty_original_lattice_comparison
       {P : Type} [Group P] [MetricSpace P] [IsIsometricSMul P P]
       (CP : LinearMetricChains P)
       (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
       (Γ : Subgroup P) (hΓ : Γ.FiniteIndex)
       (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
       (hΛ : IsUniformLattice Λ) (iso : Γ ≃* Λ) (dS : ProperChainMetric S.carrier) :
       letI := dS.compatibleMetric
   …

   Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric