OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanHomLinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Linear logarithms of homomorphisms on the actual Cartan factor

  1. theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_linearMap_on_cartan line 25

    Source documentation

    A continuous additive-target homomorphism is real-linear on Cartan logarithms, derived from the published finite BCH identity.

    theorem exists_linearMap_on_cartan
    (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) :
    ∃ A : H →ₗ[ℝ] W, ∀ v : H, A v = (l (Exp v)).toAdd := by
…

    Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput