OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialHomLinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_linearMap_of_exponential_hom line 20

   Source documentation

   Finite polynomial exponential coordinates and continuity suffice to linearize a homomorphism into an additive real vector space.

   theorem exists_linearMap_of_exponential_hom {n c : ℕ} (b : Basis (Fin n) ℝ L)
       (Exp : L → G) (hinj : Function.Injective Exp) (hzero : Exp 0 = 1)
       (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
       (hcont : Continuous (fun x : Fin n → ℝ => Exp (b.equivFun.symm x)))
       (coeff : DynkinCoefficients c 2)
       (hmul : ∀ x y, Exp (finiteDynkinPolynomial coeff ![x, y]) = Exp x * Exp y)
       (l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd) :
       ∃ A : L →ₗ[ℝ] W, ∀ x, A x = (l (Exp x)).toAdd := by
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial