IntrinsicHeightKernel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The closed nilpotent height kernel without a global ambient chart

A product of exponential curves supplies a smooth height section. The inverse function theorem identifies the integrated nilpotent model locally with the kernel. The section retracts the ambient group onto the actual kernel, so simple connectedness upgrades that local identification to a closed embedding.

theorem OAI.PolycyclicRecognition.exists_closed_intrinsic_height_kernel line 34
theorem OAI.PolycyclicRecognition.exponential_eq_one_iff_of_intrinsic_height_kernel line 115
Source documentation
A period must lie in the height kernel, whose nilpotent exponential coordinates and closed inclusion have both been constructed.
```
theorem exponential_eq_one_iff_of_intrinsic_height_kernel
    (x : GroupLieAlgebra (𝓘(ℝ, E)) G) : Exp x = 1 ↔ x = 0 := by
…
```
theorem OAI.PolycyclicRecognition.exponential_injOn_intrinsic_height_kernel line 142
Source documentation
The exponential is injective on the entire canonical height kernel.
```
theorem exponential_injOn_intrinsic_height_kernel :
    InjOn Exp (T.kernelIdeal : Set (GroupLieAlgebra (𝓘(ℝ, E)) G)) := by
…
```
theorem OAI.PolycyclicRecognition.exponential_eq_of_mem_intrinsic_height_kernel line 160
Source documentation
A kernel point has no other exponential preimage in the ambient algebra.
```
theorem exponential_eq_of_mem_intrinsic_height_kernel
    {x y : GroupLieAlgebra (𝓘(ℝ, E)) G} (hx : x ∈ T.kernelIdeal)
    (he : Exp x = Exp y) : x = y := by
…
```