OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanConeGroup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanWordModel.coneProjection line 20

   Source documentation

   The canonical Lie algebra projection onto the mixed-word quotient.

   def coneProjection (C : Set (H →ₗ[ℝ] ℝ)) :
       cartanRootIdeal H →ₗ⁅ℝ⁆ (cartanRootIdeal H) ⧸ M.coneWordIdeal C :=
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneProjection_surjective line 24
3. theorem OAI.PolycyclicRecognition.CartanWordModel.coneQuotient_nilpotent line 28
4. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_group_quotient line 36

   Source documentation

   Lie correspondence supplies the quotient group, while the actual algebra projection supplies its surjective group map and compact lifts. The kernel is precisely the exponential image of the mixed-word ideal.

   theorem exists_cone_group_quotient
       (C : Set (H →ₗ[ℝ] ℝ))
       (N : NilpotentLieModel (cartanRootIdeal H))
       (ExpN : GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier → N.carrier)
       (hExpN : IsGroupExponential ExpN)
       (haarN : NilpotentExponentialHaarInput N.modelSpace N.carrier)
       (existQ : NilpotentLieExistenceInput ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
       (haarQ : ∀ Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C),
         NilpotentExponentialHaarInput Q.modelSpace Q.carrier)
       (integrate : ∀ Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C),
         NilpotentLieIntegrationInput (EN := N.modelSpace) (N := N.carrier)
   …

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