OAI/GroupTheory/PolycyclicRecognition/Analysis/TriangulableMetricChoice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing the endpoint metrics after the topological model reduction

  1. theorem OAI.PolycyclicRecognition.exists_realTriangulable_model_with_metric_choice line 13

    Source documentation

    The topological model can be fixed before either endpoint metric. This permits selecting a minimizing-path metric on the Lie model while retaining the comparison through the two locally compact intermediate groups.

    theorem exists_realTriangulable_model_with_metric_choice
    (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