WeightRotationCharacter.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A compact rotation character on the actual adjoint-weight quotient

theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.realPhaseVector_eq_of_weightMap_eq line 20
Source documentation
The rotations do not depend on the chosen Cartan representative.
```
theorem realPhaseVector_eq_of_weightMap_eq (h k : H)
    (hh : T.weightMap (h : L) = T.weightMap (k : L)) :
    realPhaseVector L H h = realPhaseVector L H k := by
…
```
Mentions: OAI.PolycyclicRecognition.realPhaseVector
def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightRotationCharacter line 45
Source documentation
The rotational character on the image of the full complex adjoint weight map, viewed as a real additive vector group.
```
def weightRotationCharacter : Multiplicative T.weightMap.range →* realRotationTorus L H :=
…
```
Mentions: OAI.PolycyclicRecognition.realRotationTorus
def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.liftRotationCharacter line 49
Source documentation
Compose the rotation character with a group-valued weight map.
```
def liftRotationCharacter {G : Type*} [Group G]
    (q : G →* Multiplicative T.weightMap.range) : G →* realRotationTorus L H :=
…
```
Mentions: OAI.PolycyclicRecognition.realRotationTorus
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightRotationCharacter_cartan line 53
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.continuous_weightRotationCharacter line 67
Source documentation
The character is continuous for the actual finite-dimensional quotient topology; no discrete replacement of the compact torus is used.
```
theorem continuous_weightRotationCharacter : Continuous (T.weightRotationCharacter H) :=
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.continuous_liftRotationCharacter line 71