ExponentialHeightKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The group height kernel from exponential coordinates

A representation strictly upper triangular on the canonical Lie kernel is unipotent on the group height kernel. Thus the already proved chain-packing theorem applies without a separate group-kernel hypothesis.

theorem OAI.PolycyclicRecognition.integrated_height_surjective line 31
theorem OAI.PolycyclicRecognition.integrated_height_isQuotientMap line 41
Source documentation
In global exponential coordinates the height map is a quotient map. This uses only the finite-dimensional open mapping theorem, so no separate openness hypothesis on the integrated homomorphism is needed.
```
theorem integrated_height_isQuotientMap
    [TopologicalSpace L] [IsTopologicalAddGroup L] [ContinuousSMul ℝ L]
    [T2Space L] [FiniteDimensional ℝ L] [TopologicalSpace G]
    (e : L ≃ₜ G) (he : ∀ x, Exp x = e x) :
    Topology.IsQuotientMap (fun g => (π g).toAdd) := by
…
```
theorem OAI.PolycyclicRecognition.unipotent_height_kernel_of_exponential_representation line 60

theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_exponential_representation line 78

Source documentation

Polynomial chain packing for the integrated canonical height follows from a compatible triangular representation and its Lie-kernel strictness.

theorem polynomialBoundedChainPacking_of_exponential_representation
    [MetricSpace G] [IsIsometricSMul G G] [ProperSpace G] [DecidableEq G]
    (hExp : Function.Surjective Exp) {m : ℕ} [NeZero m]
    (ρ : G →* positiveTriangular m) (j : L →ₗ[ℝ] Matrix (Fin m) (Fin m) ℝ)
    (hρExp : ∀ x, matrix (ρ (Exp x)) = NormedSpace.exp (j x))
    (hstrict : ∀ x ∈ T.kernelIdeal, StrictUpper (j x))
    (hquot : Topology.IsQuotientMap (fun g => (π g).toAdd))
    (hρ : Topology.IsInducing (fun g => matrix (ρ g))) :
    PolynomialBoundedChainPacking (fun g => (π g).toAdd) := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.StrictUpper, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking

theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_exponential_chart line 94

Source documentation

The exponential-coordinate version of the packing bridge has no assumed topological quotient property and no assumed group-kernel unipotence.

theorem polynomialBoundedChainPacking_of_exponential_chart
    [TopologicalSpace L] [IsTopologicalAddGroup L] [ContinuousSMul ℝ L]
    [T2Space L] [FiniteDimensional ℝ L]
    [MetricSpace G] [IsIsometricSMul G G] [ProperSpace G] [DecidableEq G]
    (e : L ≃ₜ G) (he : ∀ x, Exp x = e x) {m : ℕ} [NeZero m]
    (ρ : G →* positiveTriangular m) (j : L →ₗ[ℝ] Matrix (Fin m) (Fin m) ℝ)
    (hρExp : ∀ x, matrix (ρ (Exp x)) = NormedSpace.exp (j x))
    (hstrict : ∀ x ∈ T.kernelIdeal, StrictUpper (j x))
    (hρ : Topology.IsInducing (fun g => matrix (ρ g))) :
    PolynomialBoundedChainPacking (fun g => (π g).toAdd) := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.StrictUpper, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking