OAI/GroupTheory/PolycyclicRecognition/Algebra/ConeIdealGroup.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual simply connected group of a cone ideal

The mixed ideal integrates to the kernel of the constructed quotient map. This provides its intrinsic Haar measure and polynomial exponential coordinates for the ideal boxes.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdeal_nilpotent line 21
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_ideal_group line 30

    Source documentation

    Lie correspondence realizes the mixed ideal as exactly the kernel of the already constructed quotient, with a closed embedding into the nilpotent factor and the correct intrinsic exponential.

    theorem exists_cone_ideal_group
    (C : Set (H →ₗ[ℝ] ℝ))
    (N : NilpotentLieModel (cartanRootIdeal H))
    (ExpN : GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier → N.carrier)
    (hExpN : IsGroupExponential ExpN)
    (haarN : NilpotentExponentialHaarInput N.modelSpace N.carrier)
    {Q : Type*} [Group Q] (π : N.carrier →* Q)
    (hker : (π.ker : Set N.carrier) =
      ExpN '' (N.equiv '' (M.coneWordIdeal C : Set (cartanRootIdeal H))))
    (existI : NilpotentLieExistenceInput (M.coneWordIdeal C))
    (haarI : ∀ I : NilpotentLieModel (M.coneWordIdeal C),
      NilpotentExponentialHaarInput I.modelSpace I.carrier)
…

    Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentLieExistenceInput