RealTorusAdjoint.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compact Cartan rotations commute with the Cartan adjoint action

theorem OAI.PolycyclicRecognition.realTorusOperator_cartan_bracket line 18

Source documentation

A rotation fixing the Cartan algebra commutes with every Cartan bracket.

theorem realTorusOperator_cartan_bracket
    (z : realRotationTorus (GroupLieAlgebra (𝓘(ℝ, E)) G) H) (h : H)
    (x : GroupLieAlgebra (𝓘(ℝ, E)) G) :
    realTorusOperator _ H z ⁅(h : GroupLieAlgebra (𝓘(ℝ, E)) G), x⁆ =
      ⁅(h : GroupLieAlgebra (𝓘(ℝ, E)) G), realTorusOperator _ H z x⁆ := by
…

Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.realTorusOperator

theorem OAI.PolycyclicRecognition.realTorusOperator_commutes_adjoint_exponential line 26
Source documentation
The same commutation holds for the exponential of the adjoint operator.
```
theorem realTorusOperator_commutes_adjoint_exponential
    (z : realRotationTorus (GroupLieAlgebra (𝓘(ℝ, E)) G) H) (h : H) (x : E) :
    realTorusOperator _ H z (NormedSpace.exp (groupAdjointOperator (E := E) (G := G) h) x) =
…
```
Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.realTorusOperator, OAI.PolycyclicRecognition.groupAdjointOperator
theorem OAI.PolycyclicRecognition.realTorusOperator_commutes_cartan_conjugation line 39
Source documentation
In the original Lie group the compact rotations commute with conjugation by exponentials of Cartan elements, at the tangent level.
```
theorem realTorusOperator_commutes_cartan_conjugation
    {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
    (z : realRotationTorus (GroupLieAlgebra (𝓘(ℝ, E)) G) H) (h : H) (x : E) :
    realTorusOperator _ H z (adjointLinearMap (E := E) (G := G) (Exp h) x) =
…
```
Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.realTorusOperator, OAI.PolycyclicRecognition.adjointLinearMap