OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanMeanFactorization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_height_factor_of_cartan_domination line 33

   Source documentation

   Segment domination, root-factor vanishing, and actual Cartan polynomial coordinates give an invertible factor on every point of the ambient group.

   theorem exists_height_factor_of_cartan_domination
       (hbijN : Function.Bijective F.ExpN)
       (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
       (hchartD : ∀ x, chartD x = F.ExpD x)
       (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
       (l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd)
       (hroot : ∀ n, l (F.inclusionN n) = 1)
       (hdom : ∀ v : H,
         (M.supportIn T hunimod eW).segmentSupport (π (Exp v)).toAdd ≤
           (M.supportIn T hunimod eW).segmentSupport (l (Exp v)).toAdd) :
       ∃ A : W ≃ₗ[ℝ] W, ∀ g, (l g).toAdd = A (π g).toAdd := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput