LinearNilpotentKernel.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Closed nilpotent kernels of linear exponential quotients

This is the kernel construction used for the complex diagonal weights in a general solvable group. It needs only a surjective linear quotient, its exponential-compatible group homomorphism, and nilpotence of its Lie kernel.

theorem OAI.PolycyclicRecognition.exists_closed_linear_nilpotent_kernel line 25

Source documentation

The integrated simply connected nilpotent model is a closed embedded copy of the actual group kernel.

theorem exists_closed_linear_nilpotent_kernel
    (I : LieIdeal ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)) (hI : LieRing.IsNilpotent I)
    (d : E →ₗ[ℝ] W) (hd : Function.Surjective d)
    (hker : LinearMap.ker d = I.toSubmodule)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W) (hπ : Continuous π)
    (he : ∀ 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