NilpotentAutomorphism.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Integrating the needed nilpotent automorphisms

The finite published Dynkin identity and bijectivity of the intrinsic exponential suffice to integrate any Lie automorphism of the nilpotent model. No general Lie-integration theorem is assumed here.

def OAI.PolycyclicRecognition.exponentialConjugate line 27
Source documentation
Conjugation through the intrinsic exponential as a bijection.
```
def exponentialConjugate (F : L ≃ₗ⁅ℝ⁆ L) : G ≃ G :=
…
```
theorem OAI.PolycyclicRecognition.exponentialConjugate_apply_exp line 32

theorem OAI.PolycyclicRecognition.exponentialConjugate_map_mul line 40

Source documentation

A finite Lie polynomial commutes with F, so the same Dynkin formula on both sides proves multiplicativity after exponentiation.

theorem exponentialConjugate_map_mul
    (dynkin : NilpotentDynkinExpansionInput E G) (hExp : IsGroupExponential Exp)
    {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥)
    (F : L ≃ₗ⁅ℝ⁆ L) (g k : G) :
    exponentialConjugate e Exp hbij F (g * k) =
      exponentialConjugate e Exp hbij F g * exponentialConjugate e Exp hbij F k := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.exponentialConjugate

def OAI.PolycyclicRecognition.integrateNilpotentLieEquiv line 68

Source documentation

The group automorphism needed for exact weight dilation.

def integrateNilpotentLieEquiv
    (dynkin : NilpotentDynkinExpansionInput E G) (hExp : IsGroupExponential Exp)
    {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥) (F : L ≃ₗ⁅ℝ⁆ L) : G ≃* G where
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput

theorem OAI.PolycyclicRecognition.integrateNilpotentLieEquiv_apply_exp line 74