OAI/GroupTheory/PolycyclicRecognition/Geometry/ComplexWeightKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_closed_complex_weight_kernel line 23

   Source documentation

   The nilpotent infinitesimal weight kernel integrates onto the full kernel of a continuous character on the original group.

   theorem exists_closed_complex_weight_kernel :
       ∃ π : G →* Multiplicative T.weightMap.range, Continuous π ∧
         (∀ x, (π (Exp x)).toAdd = T.weightMap.rangeRestrict x) ∧
         ∃ (N : NilpotentLieModel T.kernelIdeal)
           (ExpN : GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier → N.carrier),
           IsGroupExponential ExpN ∧
           ∃ ι : N.carrier →* G, Topology.IsClosedEmbedding ι ∧
             ContMDiff (𝓘(ℝ, N.modelSpace)) (𝓘(ℝ, E)) ∞ ι ∧
             (∀ x : T.kernelIdeal, ι (ExpN (N.equiv x)) = Exp x) ∧
             Set.range ι = (π.ker : Set G) := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentLieModel