ExponentialRepresentationInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exponential compatibility in the published faithful realization

Onshuus–Post (2022), Proposition 2.4 and proof, give a faithful inducing linear Lie realization of a simply connected real triangular group. Lee, Introduction to Smooth Manifolds, second edition (2013), Theorem 8.44 (p.195) and Proposition 20.8(g) (p.520), give its Lie algebra map and exponential compatibility. Only these properties are retained below.

https://doi.org/10.1112/blms.12574 https://doi.org/10.1007/978-1-4419-9982-5

The action and all bounds remain proved consequences, not part of the input.

def OAI.PolycyclicRecognition.ExponentialLinearRealizationInput line 35
Source documentation
Faithful linear realization with its intrinsic exponential identity. No metric distortion estimate is included.
```
def ExponentialLinearRealizationInput [SimplyConnectedSpace G] : Prop :=
…
```
theorem OAI.PolycyclicRecognition.cartan_action_eq_adjoint_of_published_realization line 51
Source documentation
The published representation identifies the actual factor action with the explicit full Cartan adjoint automorphism.
```
theorem cartan_action_eq_adjoint_of_published_realization
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.exists_ambient_word_box_bound_of_published_inputs line 75
Source documentation
The ambient word estimate now depends only on the published exponential, Dynkin and representation inputs. No action or factor-path estimate is an extra premise.
```
theorem exists_ambient_word_box_bound_of_published_inputs
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.exists_ambient_word_factor_bound_of_published_inputs line 112
Source documentation
The ambient word estimate now depends only on the published exponential, Dynkin and representation inputs. No action or factor-path estimate is an extra premise.
```
theorem exists_ambient_word_factor_bound_of_published_inputs
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput