OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoverRootDistortion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic root distortion in the genuine Cartan cover

Ambient conjugation identities lift to the nilpotent coordinate because its inclusion is injective. No injectivity of the whole cover projection is used.

  1. def OAI.PolycyclicRecognition.CartanFactorModel.semidirectRootExp line 32

    Source documentation

    The root exponential in the first coordinate of the semidirect cover.

    def CartanFactorModel.semidirectRootExp
    (χ : Weight ℝ H (GroupLieAlgebra (𝓘(ℝ, EG)) G)) (hχ : χ.IsNonZero)
    (v : rootSpace H χ) : F.N.carrier ⋊[F.action] F.D.carrier :=
…
  2. theorem OAI.PolycyclicRecognition.CartanFactorModel.semidirect_root_logarithmic_distortion line 38