RealCartanRotations.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Cartan rotations preserve the actual real form

def OAI.PolycyclicRecognition.realCartanInComplex line 17
Source documentation
The original real Cartan algebra inside its complexification.
```
def realCartanInComplex (h : H) : complexifiedSubalgebra L H :=
…
```
Mentions: OAI.PolycyclicRecognition.complexifiedSubalgebra
theorem OAI.PolycyclicRecognition.cartanConjugation_real line 21
theorem OAI.PolycyclicRecognition.phase_conjugate_real line 27
theorem OAI.PolycyclicRecognition.complex_rotation_conjugation line 39
Source documentation
Conjugation commutes with rotations by real Cartan parameters.
```
theorem complex_rotation_conjugation (h : H) (x : ℂ ⊗[ℝ] L) :
    complexificationConjugation L
      (ComplexCartan.rotationLinear (complexifiedSubalgebra L H) (realCartanInComplex L H h) x) =
    ComplexCartan.rotationLinear (complexifiedSubalgebra L H) (realCartanInComplex L H h)
      (complexificationConjugation L x) := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationConjugation, OAI.PolycyclicRecognition.ComplexCartan.rotationLinear, OAI.PolycyclicRecognition.complexifiedSubalgebra, OAI.PolycyclicRecognition.realCartanInComplex
theorem OAI.PolycyclicRecognition.exists_real_rotation line 54
Source documentation
Each rotation of a real vector is still real.
```
theorem exists_real_rotation (h : H) (x : L) :
    ∃ y : L,
      ComplexCartan.rotationLinear (complexifiedSubalgebra L H) (realCartanInComplex L H h)
        (1 ⊗ₜ[ℝ] x) = 1 ⊗ₜ[ℝ] y := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.rotationLinear, OAI.PolycyclicRecognition.complexifiedSubalgebra, OAI.PolycyclicRecognition.realCartanInComplex
def OAI.PolycyclicRecognition.realRotationMap line 64
Source documentation
The real rotation, obtained by taking real coordinates of the complex weight rotation.
```
def realRotationMap (h : H) : L →ₗ[ℝ] L :=
…
```
theorem OAI.PolycyclicRecognition.realRotationMap_complexify line 70
theorem OAI.PolycyclicRecognition.realCartanInComplex_add line 81
theorem OAI.PolycyclicRecognition.realCartanInComplex_zero line 87
theorem OAI.PolycyclicRecognition.realRotationMap_add_apply line 91
theorem OAI.PolycyclicRecognition.realRotationMap_zero_apply line 98
theorem OAI.PolycyclicRecognition.realRotationMap_lie line 103
def OAI.PolycyclicRecognition.realCartanRotation line 115
Source documentation
Removing rotational weights uses actual automorphisms of the original real Lie algebra, with inverse given by the negative parameter.
```
def realCartanRotation (h : H) : L ≃ₗ⁅ℝ⁆ L where
…
```