CartanAdjointAction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The full exponential Cartan action

The scalar dilation and the polynomial residual automorphism together give the exponential of the actual adjoint action on every nonzero root. In a compatible faithful representation this is conjugation, not an independently assumed action on the nilpotent ideal.

def OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism line 25
Source documentation
The full Cartan action, including its nonsemisimple part.
```
def cartanIdealAdjointAutomorphism (h : H) : cartanRootIdeal H ≃ₗ⁅ℝ⁆ cartanRootIdeal H :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.cartanIdealWeightDilation_eq_of_height_eq line 28
theorem OAI.PolycyclicRecognition.rootInIdeal_adjoint_exp line 57
Source documentation
The full action is the analytic adjoint exponential on each nonzero root.
```
theorem rootInIdeal_adjoint_exp (h : H) (v : rootSpace H χ) :
    CartanWordModel.rootInIdeal χ hχ ((NormedSpace.exp (rootAction H χ h)) v) =
      cartanIdealAdjointAutomorphism T H h (CartanWordModel.rootInIdeal χ hχ v) := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal, OAI.PolycyclicRecognition.rootAction, OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism
theorem OAI.PolycyclicRecognition.represented_adjoint_root line 77
Source documentation
The constructed action agrees with conjugation in a compatible algebra representation on every generating root.
```
theorem represented_adjoint_root (j : L →ₗ⁅ℝ⁆ A) (h : H) (v : rootSpace H χ) :
    j (cartanIdealAdjointAutomorphism T H h (CartanWordModel.rootInIdeal χ hχ v) : L) =
      NormedSpace.exp (j h) * j v * NormedSpace.exp (-j h) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism, OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal
theorem OAI.PolycyclicRecognition.represented_adjoint_ideal line 88
Source documentation
Lie generation extends the root calculation to every vector in the nilpotent ideal.
```
theorem represented_adjoint_ideal (j : L →ₗ⁅ℝ⁆ A) (h : H) (x : cartanRootIdeal H) :
    j (cartanIdealAdjointAutomorphism T H h x : L) =
      NormedSpace.exp (j h) * j x * NormedSpace.exp (-j h) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism