TriangulableLieModel.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The published reduction to a real-triangulable Lie model

Y. Cornulier and R. Tessera, Geometric presentations of Lie groups and their Dehn functions, Publications Mathématiques de l'IHÉS 125 (2017), 79–219, Lemma 3.A.1, p.108, gives proper continuous homomorphisms with cocompact images G ← G₁ → G₂ ← G₃, with G₃ real triangulable. Definition 1.1, p.83, identifies this last property with being isomorphic to a closed connected group of invertible upper triangular real matrices.

The input below keeps precisely that topological reduction. Its metric consequence is proved using the separately identified compatible-metric existence input and the explicit inverse-map composition lemmas. No adjoint basis, height control, or recognition conclusion is placed in the published input.

def OAI.PolycyclicRecognition.IsRealTriangulable line 31
Source documentation
The actual closed triangular matrix realization from CT Definition 1.1.
```
def IsRealTriangulable (S : SimplyConnectedSolvableLieModel) : Prop :=
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel
structure OAI.PolycyclicRecognition.CompactlyGeneratedLCModel line 38
Source documentation
Only the locally compact group data used from an intermediate Lie group in the CT reduction; the smooth structure is unnecessary here.
```
structure CompactlyGeneratedLCModel where
…
```
structure OAI.PolycyclicRecognition.ProperCocompactHom line 54
Source documentation
A proper continuous homomorphism whose image has a compact coset cover, the cocompactness condition in the CT arrows.
```
structure ProperCocompactHom (A B : Type*) [Group A] [Group B]
    [TopologicalSpace A] [TopologicalSpace B] where
…
```
def OAI.PolycyclicRecognition.CornulierTesseraModelInput line 64
Source documentation
The solvable-source specialization of CT Lemma 3.A.1. The intermediate Lie groups are retained only through the locally compact data needed to compare their metrics.
```
def CornulierTesseraModelInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.ProperCocompactHom.nonempty_metricQuasiEquivalence line 74
Source documentation
Compatible metrics turn one of the topological arrows into actual coarse inverse maps.
```
theorem ProperCocompactHom.nonempty_metricQuasiEquivalence
    {A B : Type*} [Group A] [Group B] [TopologicalSpace A] [TopologicalSpace B]
    (f : ProperCocompactHom A B) (dA : ProperChainMetric A) (dB : ProperChainMetric B) :
    letI := dA.compatibleMetric
…
```
Mentions: OAI.PolycyclicRecognition.ProperCocompactHom, OAI.PolycyclicRecognition.ProperChainMetric
theorem OAI.PolycyclicRecognition.exists_realTriangulable_metric_model line 94
Source documentation
The metric reduction follows from the precise topological CT input: choose compatible metrics and compose the three arrows with their actual coarse inverses.
```
theorem exists_realTriangulable_metric_model
    (ct : CornulierTesseraModelInput) (metricInput : GeodesicMetricExistenceInput)
    (S : SimplyConnectedSolvableLieModel) :
    ∃ T : SimplyConnectedSolvableLieModel, IsRealTriangulable T ∧
      ∃ (dS : ProperChainMetric S.carrier) (dT : ProperChainMetric T.carrier),
        letI := dS.compatibleMetric
…
```
Mentions: OAI.PolycyclicRecognition.CornulierTesseraModelInput, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsRealTriangulable, OAI.PolycyclicRecognition.ProperChainMetric