CanonicalHeightIntegration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Integrating the canonical height

J. M. Lee, Introduction to Smooth Manifolds, second edition, GTM 218, Springer (2013), Theorem 20.19, p.530, integrates a Lie algebra homomorphism from a simply connected group. Proposition 20.8(g), p.520, gives compatibility with the exponential. We retain just the real-valued character specialization: a real linear form vanishing on brackets integrates to a continuous additive character. This is the same published integration theorem as in NilpotentLieIntegrationInput, with an arbitrary simply connected source and the one-dimensional abelian target. No height quotient, Lipschitz bound or recognition conclusion is assumed in this input.

The diagonal characters are already proved to kill brackets. Integrating them and using the existing global exponential chart constructs the actual height homomorphism. Its continuity, surjectivity, quotient property and global Lipschitz bound are then proved.

Primary text: https://math.berkeley.edu/~jchaidez/materials/reu/lee_smooth_manifolds.pdf

def OAI.PolycyclicRecognition.ScalarCharacterIntegrationInput line 40
Source documentation
The scalar-target specialization of Lee 20.19 and 20.8(g).
```
def ScalarCharacterIntegrationInput [T2Space G] [SecondCountableTopology G] : Prop :=
…
```
theorem OAI.PolycyclicRecognition.exists_canonical_height_of_exponential_chart line 55
Source documentation
Integrated scalar characters make the logarithmic quotient formula into an actual continuous group homomorphism. No group law for the logarithm is assumed.
```
theorem exists_canonical_height_of_exponential_chart
    (integrate : ScalarCharacterIntegrationInput (E := E) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ScalarCharacterIntegrationInput
theorem OAI.PolycyclicRecognition.exists_lipschitz_canonical_height line 115
Source documentation
The published scalar integration and global exponential inputs supply the actual canonical height with all metric compatibility hypotheses used by the transferred-height argument.
```
theorem exists_lipschitz_canonical_height
    (chains : LinearMetricChains G)
    (integrate : ScalarCharacterIntegrationInput (E := E) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ScalarCharacterIntegrationInput