ComplexCartanRotations.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Rotations on complex Cartan weight spaces

The imaginary parts of the generalized weights define genuine Lie algebra automorphisms. Their coefficient vectors lie in a fixed compact torus. These are the rotations to be removed in the real-triangulable model construction.

def OAI.PolycyclicRecognition.ComplexCartan.weightDecomposition line 27
Source documentation
The generalized Cartan decomposition over the complex numbers.
```
def weightDecomposition :
    (⨁ χ : Weight ℂ H L, (genWeightSpace L χ).toSubmodule) ≃ₗ[ℂ] L := by
…
```
def OAI.PolycyclicRecognition.ComplexCartan.weightOperator line 37
Source documentation
A scalar on each generalized weight block.
```
def weightOperator (z : Weight ℂ H L → ℂ) : L →ₗ[ℂ] L := by
…
```
theorem OAI.PolycyclicRecognition.ComplexCartan.weightOperator_apply line 43
theorem OAI.PolycyclicRecognition.ComplexCartan.root_induction line 55
def OAI.PolycyclicRecognition.ComplexCartan.imaginaryPart line 65
Source documentation
The imaginary part, viewed as a purely imaginary complex number.
```
def imaginaryPart : ℂ →ₗ[ℝ] ℂ where
…
```
def OAI.PolycyclicRecognition.ComplexCartan.phase line 71
Source documentation
Rotational scalar on a weight block.
```
def phase (h : H) (χ : H → ℂ) : ℂ := Complex.exp (imaginaryPart (χ h))
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.imaginaryPart
theorem OAI.PolycyclicRecognition.ComplexCartan.norm_phase line 74
def OAI.PolycyclicRecognition.ComplexCartan.rotationLinear line 77
theorem OAI.PolycyclicRecognition.ComplexCartan.rotationLinear_apply line 79
theorem OAI.PolycyclicRecognition.ComplexCartan.rotationLinear_apply_genWeight line 83
theorem OAI.PolycyclicRecognition.ComplexCartan.phase_add_weight line 91
theorem OAI.PolycyclicRecognition.ComplexCartan.phase_add line 95
theorem OAI.PolycyclicRecognition.ComplexCartan.phase_zero line 99
theorem OAI.PolycyclicRecognition.ComplexCartan.rotationLinear_map_lie line 102
theorem OAI.PolycyclicRecognition.ComplexCartan.rotationLinear_add_apply line 120
theorem OAI.PolycyclicRecognition.ComplexCartan.rotationLinear_zero_apply line 130
def OAI.PolycyclicRecognition.ComplexCartan.rotation line 140
Source documentation
Rotation is an actual Lie automorphism, inverted by negating the Cartan parameter, with no semisimplicity assumption on the original Cartan action.
```
def rotation (h : H) : L ≃ₗ⁅ℂ⁆ L where
…
```

theorem OAI.PolycyclicRecognition.ComplexCartan.phase_coefficients_precompact line 151

Source documentation

All rotational coefficient vectors lie in one compact set.

theorem phase_coefficients_precompact :
    IsCompact {z : Weight ℂ H L → ℂ | ∀ χ, ‖z χ‖ = 1} ∧
      ∀ h : H, (fun χ : Weight ℂ H L => phase H h χ) ∈
        {z : Weight ℂ H L → ℂ | ∀ χ, ‖z χ‖ = 1} := by
…

Mentions: OAI.PolycyclicRecognition.ComplexCartan.phase