RealRotationDerivation.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Infinitesimal Cartan rotations on the real Lie algebra

theorem OAI.PolycyclicRecognition.complex_imaginaryOperator_conjugation line 17
Source documentation
Conjugation respects the imaginary semisimple part for real parameters.
```
theorem complex_imaginaryOperator_conjugation (h : H) (x : ℂ ⊗[ℝ] L) :
    complexificationConjugation L
      (ComplexCartan.imaginaryOperator (complexifiedSubalgebra L H) (realCartanInComplex L H h) x) =
    ComplexCartan.imaginaryOperator (complexifiedSubalgebra L H) (realCartanInComplex L H h)
      (complexificationConjugation L x) := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationConjugation, OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator, OAI.PolycyclicRecognition.complexifiedSubalgebra, OAI.PolycyclicRecognition.realCartanInComplex
theorem OAI.PolycyclicRecognition.exists_real_imaginaryOperator line 34
Source documentation
The imaginary operator preserves the embedded real form.
```
theorem exists_real_imaginaryOperator (h : H) (x : L) :
    ∃ y : L, ComplexCartan.imaginaryOperator (complexifiedSubalgebra L H)
      (realCartanInComplex L H h) (1 ⊗ₜ[ℝ] x) = 1 ⊗ₜ[ℝ] y := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryOperator, OAI.PolycyclicRecognition.complexifiedSubalgebra, OAI.PolycyclicRecognition.realCartanInComplex
def OAI.PolycyclicRecognition.realImaginaryOperator line 43
Source documentation
The real imaginary semisimple operator, obtained from the actual complex weight spaces by real descent.
```
def realImaginaryOperator (h : H) : L →ₗ[ℝ] L :=
…
```
theorem OAI.PolycyclicRecognition.realImaginaryOperator_complexify line 49
theorem OAI.PolycyclicRecognition.realImaginaryOperator_lie line 59
def OAI.PolycyclicRecognition.realImaginaryDerivation line 74
Source documentation
The infinitesimal compact action as a real derivation.
```
def realImaginaryDerivation (h : H) : LieDerivation ℝ L L where
…
```
theorem OAI.PolycyclicRecognition.realImaginaryOperator_add line 80
theorem OAI.PolycyclicRecognition.realImaginaryOperator_zero line 89
theorem OAI.PolycyclicRecognition.realImaginaryOperator_cartan line 95
theorem OAI.PolycyclicRecognition.realCartanInComplex_real_smul line 104
Source documentation
The real embedding is linear in the Cartan parameter.
```
theorem realCartanInComplex_real_smul (r : ℝ) (h : H) :
    realCartanInComplex L H (r • h) = r • realCartanInComplex L H h := by
…
```
Mentions: OAI.PolycyclicRecognition.realCartanInComplex
theorem OAI.PolycyclicRecognition.realImaginaryOperator_smul line 110
theorem OAI.PolycyclicRecognition.realImaginaryOperator_commute line 119
def OAI.PolycyclicRecognition.realImaginaryDerivationLinear line 129
Source documentation
The imaginary derivation depends linearly on the real Cartan parameter.
```
def realImaginaryDerivationLinear : H →ₗ[ℝ] LieDerivation ℝ L L where
…
```