LieModelMetric.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Compatible metrics for the solvable Lie model

The metric existence input is the precise specialization of Cornulier–de la Harpe, Metric Geometry of Locally Compact Groups, EMS Tracts in Mathematics 25 (2016), Proposition 4.B.9, p.108: a second-countable locally compact group is compactly generated if and only if it admits a proper compatible left-invariant large-scale-geodesic metric.

We prove compact generation from a compact identity neighborhood and connectedness. The metric-existence input is separate from Dekimpe's lattice-realization theorem and contains no recognition assertion.

structure OAI.PolycyclicRecognition.ProperChainMetric line 30
Source documentation
A compatible proper left-invariant metric together with its explicit large-scale-geodesic chains.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:125 (same declaration text).
```
structure ProperChainMetric (G : Type*) [Group G] [TopologicalSpace G] where
…
```
abbrev OAI.PolycyclicRecognition.ProperChainMetric.compatibleMetric line 43
Source documentation
Normalize the metric so that its topology is definitionally the original topology; the existing Lie charts then remain usable.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:133 (different declaration text). Qualify references as OAI.PolycyclicRecognition.ProperChainMetric.compatibleMetric@path.
```
abbrev compatibleMetric : MetricSpace G :=
…
```
theorem OAI.PolycyclicRecognition.ProperChainMetric.compatibleMetric_eq line 46
theorem OAI.PolycyclicRecognition.ProperChainMetric.proper_compatibleMetric line 49
theorem OAI.PolycyclicRecognition.ProperChainMetric.isometric_compatibleMetric line 53
def OAI.PolycyclicRecognition.ProperChainMetric.chains_compatibleMetric line 57

theorem OAI.PolycyclicRecognition.closure_eq_top_of_mem_nhds_one line 65

Source documentation

Any compact identity neighborhood in a connected topological group generates the entire group.

theorem closure_eq_top_of_mem_nhds_one
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [ConnectedSpace G] {K : Set G} (hK : K ∈ 𝓝 (1 : G)) :
    Subgroup.closure K = ⊤ := by
…

theorem OAI.PolycyclicRecognition.exists_compact_generating_set line 77

Source documentation

A connected locally compact group has a compact generating set.

theorem exists_compact_generating_set
    (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [ConnectedSpace G] [LocallyCompactSpace G] :
    ∃ K : Set G, IsCompact K ∧ Subgroup.closure K = ⊤ := by
…

def OAI.PolycyclicRecognition.GeodesicMetricExistenceInput line 86
Source documentation
The implication (i)⇒(ii) of Cornulier–de la Harpe (2016), Proposition 4.B.9, with the chain witnesses retained.
```
def GeodesicMetricExistenceInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel.nonempty_properChainMetric line 94
Source documentation
Connectedness discharges the compact-generation hypothesis of the published metric-existence theorem for the solvable Lie model.
```
theorem SimplyConnectedSolvableLieModel.nonempty_properChainMetric
    (S : SimplyConnectedSolvableLieModel) (metricInput : GeodesicMetricExistenceInput) :
    Nonempty (ProperChainMetric S.carrier) := by
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.ProperChainMetric