ComplexRotationTorus.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The compact group containing the Cartan rotations

Diagonal unit scalars are invertible on the generalized weight decomposition. The equations for preserving the bracket and fixing the Cartan algebra cut out an actual closed subgroup of a finite torus, giving a compact action.

def OAI.PolycyclicRecognition.ComplexCartan.weightOperatorLinear line 24
Source documentation
Linear dependence of a block diagonal operator on its coefficients.
```
def weightOperatorLinear : (Weight ℂ H L → ℂ) →ₗ[ℂ] Module.End ℂ L where
…
```
def OAI.PolycyclicRecognition.ComplexCartan.torusOperator line 45
Source documentation
A unit diagonal coefficient vector acts on the entire algebra.
```
def torusOperator (z : Weight ℂ H L → Circle) : Module.End ℂ L :=
…
```
theorem OAI.PolycyclicRecognition.ComplexCartan.torusOperator_one line 48
theorem OAI.PolycyclicRecognition.ComplexCartan.torusOperator_mul line 57
theorem OAI.PolycyclicRecognition.ComplexCartan.torusOperator_injective line 67
def OAI.PolycyclicRecognition.ComplexCartan.rotationTorus line 74
Source documentation
Bracket-preserving unit coefficient vectors that fix the Cartan algebra.
```
def rotationTorus : Subgroup (Weight ℂ H L → Circle) where
…
```
def OAI.PolycyclicRecognition.ComplexCartan.torusAutomorphism line 99
Source documentation
Each element of the compact coefficient group is a Lie automorphism.
```
def torusAutomorphism (z : rotationTorus H) : L ≃ₗ⁅ℂ⁆ L where
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.rotationTorus
def OAI.PolycyclicRecognition.ComplexCartan.phaseVector line 109
Source documentation
The genuine Cartan rotations belong to this subgroup.
```
def phaseVector (h : H) : rotationTorus H := by
…
```
Mentions: OAI.PolycyclicRecognition.ComplexCartan.rotationTorus
def OAI.PolycyclicRecognition.ComplexCartan.bracketOperator line 134
def OAI.PolycyclicRecognition.ComplexCartan.coefficientOperator line 141
Source documentation
The continuous operator associated to the finite coefficient vector.
```
def coefficientOperator : (Weight ℂ H L → ℂ) →ₗ[ℂ] (L →L[ℂ] L) :=
…
```
theorem OAI.PolycyclicRecognition.ComplexCartan.coefficientOperator_apply line 145
theorem OAI.PolycyclicRecognition.ComplexCartan.continuous_torusOperator line 148
theorem OAI.PolycyclicRecognition.ComplexCartan.rotationTorus_isClosed line 154
instance OAI.PolycyclicRecognition.ComplexCartan.rotationTorus_compactSpace line 167