GeneratorConjugation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual group words realizing a basis of generator conjugates

A faithful exponential-compatible representation turns the operator words from GeneratorOrbit into conjugation by finite words in generator one-parameter subgroups. No generation or submersion assertion is assumed.

def OAI.PolycyclicRecognition.generatorGroupWord line 21
Source documentation
A finite word using only the specified generator exponentials.
```
def generatorGroupWord {I L G : Type*} [SMul ℝ L] [Group G]
    (X : I → L) (Exp : L → G) (w : List (I × ℝ)) : G :=
…
```
theorem OAI.PolycyclicRecognition.generatorGroupWord_nil line 25
theorem OAI.PolycyclicRecognition.generatorGroupWord_cons line 28
theorem OAI.PolycyclicRecognition.represented_exp_continuousAd line 46
Source documentation
A Lie representation intertwines the full adjoint exponential with ordinary algebra conjugation.
```
theorem represented_exp_continuousAd (j : L →ₗ⁅ℝ⁆ A) (x v : L) (t : ℝ) :
    j (NormedSpace.exp (t • continuousAd x) v) =
      NormedSpace.exp (t • j x) * j v * NormedSpace.exp (-(t • j x)) := by
…
```
Mentions: OAI.PolycyclicRecognition.continuousAd
theorem OAI.PolycyclicRecognition.exp_ad_eq_group_conjugation line 63
Source documentation
Conjugation along one generator is the exponential of its actual adjoint.
```
theorem exp_ad_eq_group_conjugation (x v : L) (t : ℝ) :
    Exp (NormedSpace.exp (t • continuousAd x) v) =
      Exp (t • x) * Exp v * (Exp (t • x))⁻¹ := by
…
```
Mentions: OAI.PolycyclicRecognition.continuousAd
theorem OAI.PolycyclicRecognition.exp_adjointWord_eq_group_conjugation line 73
Source documentation
The whole operator word is conjugation by its matching group word.
```
theorem exp_adjointWord_eq_group_conjugation (w : List (I × ℝ)) (v : L) :
    Exp (generatorAdjointWord X w v) =
      generatorGroupWord X Exp w * Exp v * (generatorGroupWord X Exp w)⁻¹ := by
…
```
Mentions: OAI.PolycyclicRecognition.generatorAdjointWord, OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.exists_generatorGroupWord_basis line 88

Source documentation

Every finite-dimensional generated algebra has a basis of directions whose full one-parameter subgroups are generator-word conjugates.

theorem exists_generatorGroupWord_basis
    (hX : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤) :
    ∃ (b : Basis (Fin (finrank ℝ L)) ℝ L)
      (w : Fin (finrank ℝ L) → List (I × ℝ)) (i : Fin (finrank ℝ L) → I),
      ∀ k (t : ℝ), Exp (t • b k) =
        generatorGroupWord X Exp (w k) * Exp (t • X (i k)) *
          (generatorGroupWord X Exp (w k))⁻¹ := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord