OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialIdeal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Invariance of Lie ideals under adjoint exponentials

Closed subspaces invariant under an operator are invariant under its exponential, by the convergent power series. Together with the already proved conjugation formula in a faithful representation, this proves normality for the exponential images used by the Cartan construction.

  1. theorem OAI.PolycyclicRecognition.exp_apply_mem_of_stable line 21
  2. theorem OAI.PolycyclicRecognition.exp_continuousAd_mem_ideal line 50
  3. theorem OAI.PolycyclicRecognition.normal_of_exponential_ideal_representation line 62

    Source documentation

    Normality follows from a faithful exponential-compatible representation and surjectivity of the ambient exponential. No normality input is used.

    theorem normal_of_exponential_ideal_representation
    (Exp : L → G) (hExp : Function.Surjective Exp)
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (hρExp : ∀ x, ρ (Exp x) = algebraExpUnit (j x))
    (I : LieIdeal ℝ L) (S : Subgroup G)
    (hS : (S : Set G) = Exp '' (I : Set L)) : S.Normal := by
…

    Mentions: OAI.PolycyclicRecognition.algebraExpUnit