LieModelUnimodular.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Unimodularity of the metric Lie model

Restrict the ambient quasi-isometry to an actual uniform lattice. Its compact coset cover supplies coarse surjectivity, and its inherited metric has finite balls. The previously proved metric Følner transfer then makes the target Haar measure right invariant. No unimodularity assumption is made about either ambient group.

theorem OAI.PolycyclicRecognition.IsUniformLattice.isMulRightInvariant_of_metricQuasiEquivalence line 33
Source documentation
The compact cover of a polycyclic uniform lattice and an ambient quasi-isometry give right invariance of the target's actual Haar measure.
```
theorem IsUniformLattice.isMulRightInvariant_of_metricQuasiEquivalence
    {Λ : Subgroup S} (hΛ : IsUniformLattice Λ) (hpoly : IsPolycyclic Λ)
    (e : MetricQuasiEquivalence S G)
    (μ : Measure G) [μ.IsHaarMeasure] [Measure.InnerRegular μ] :
    μ.IsMulRightInvariant := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic, OAI.PolycyclicRecognition.MetricQuasiEquivalence
theorem OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel.isMulRightInvariant_of_lattice_comparison line 65
Source documentation
The actual Lie model obtained by the CT metric comparison is unimodular when its source contains the given uniform solvable lattice. Farb–Weinberger is used only for polycyclicity of that lattice.
```
theorem SimplyConnectedSolvableLieModel.isMulRightInvariant_of_lattice_comparison
    (fw : FarbWeinbergerLatticeInput) (S T : SimplyConnectedSolvableLieModel)
    (Λ : Subgroup S.carrier) (hΛ : IsUniformLattice Λ)
    (dS : ProperChainMetric S.carrier) (dT : ProperChainMetric T.carrier)
    (e : letI := dS.compatibleMetric
…
```
Mentions: OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric