OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFactorRepresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating a Lie representation through the Cartan factors

Uniqueness of exponential preimages meeting the root ideal suffices to descend a nilpotently integrated representation through the factor product. Global injectivity of the exponential gives a specialization.

  1. theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_integrated_representation_of_root_preimages line 29
  2. theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_integrated_representation line 115

    Source documentation

    Global injectivity of the exponential specializes the factor descent theorem.

    theorem CartanFactorModel.exists_integrated_representation
    (F : CartanFactorModel H Exp)
    (hExp : IsGroupExponential Exp) (hinj : Function.Injective Exp)
    (hn : LieRing.IsNilpotent (cartanRootIdeal H))
    (hspan : (cartanRootIdeal H).toSubmodule ⊔ H.toSubmodule = ⊤)
    (hsN : Function.Surjective F.ExpN) (hsD : Function.Surjective F.ExpD)
    (j : GroupLieAlgebra (𝓘(ℝ, E)) G →ₗ⁅ℝ⁆ A) :
    ∃ ρ : G →* Aˣ, Continuous ρ ∧ ∀ x, ρ (Exp x) = algebraExpUnit (j x) :=
…

    Mentions: OAI.PolycyclicRecognition.CartanFactorModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit