ClosedNilpotentLinearKernel.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Closed integration of a nilpotent linear kernel

The split-coordinate argument for the real height kernel also applies to the complex adjoint weights, viewed as a real linear quotient. Only nilpotence, surjectivity and the exact exponential identity are used.

theorem OAI.PolycyclicRecognition.exists_closed_nilpotent_linear_kernel line 25

Source documentation

Integrate the nilpotent kernel of an actual surjective linear group character as a closed subgroup of the given simply connected Lie group.

theorem exists_closed_nilpotent_linear_kernel
    (I : LieIdeal ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)) (hnil : LieRing.IsNilpotent I)
    (d : E →ₗ[ℝ] W) (hd : Function.Surjective d)
    (hker : ∀ x, d x = 0 ↔ x ∈ I)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W) (hπ : Continuous π)
    (hπExp : ∀ x, (π (Exp x)).toAdd = d x) :
    ∃ (N : NilpotentLieModel I)
      (ExpN : GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier → N.carrier),
      IsGroupExponential ExpN ∧
      ∃ ι : N.carrier →* G, Topology.IsClosedEmbedding ι ∧
        ContMDiff (𝓘(ℝ, N.modelSpace)) (𝓘(ℝ, E)) ∞ ι ∧
…

Mentions: OAI.PolycyclicRecognition.NilpotentLieModel