IntrinsicSmoothCoordinates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth global coordinates from the height and its nilpotent kernel

These are product coordinates from a smooth section, not a claim that the ambient exponential is surjective. They suffice for the metric contraction.

theorem OAI.PolycyclicRecognition.exists_intrinsic_smooth_product_coordinates line 26

theorem OAI.PolycyclicRecognition.exists_intrinsic_smooth_coordinates line 112

Source documentation

Reindex the product coordinates by one finite real coordinate space.

theorem exists_intrinsic_smooth_coordinates
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W) (hπ : Continuous π)
    (he : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :
    ∃ (n : ℕ) (φ : (Fin n → ℝ) ≃ₜ G), φ 0 = 1 ∧
      ContMDiff (𝓘(ℝ, Fin n → ℝ)) (𝓘(ℝ, E)) ∞ φ ∧
      ContMDiff (𝓘(ℝ, E)) (𝓘(ℝ, Fin n → ℝ)) ∞ φ.symm := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection