OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSourceDilationUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.sourceDilation_eq_of_exp line 23

   Source documentation

   Exponential surjectivity identifies a source automorphism with the canonical continuous dilation, without an extra compatibility hypothesis.

   theorem sourceDilation_eq_of_exp
       (hbij : Function.Bijective F.ExpN)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ v, chartN v = F.ExpN v)
       (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (h : H) (S : F.N.carrier ≃ₜ* F.N.carrier)
       (hS : ∀ v, S (F.ExpN (F.N.equiv v)) =
         F.ExpN (F.N.equiv (cartanIdealWeightDilation T H h v))) :
       S = M.sourceDilation T F hbij chartN hchartN dynkinN h := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanIdealWeightDilation