ComplexCartanQuotient.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact rotations act trivially on the adjoint-weight quotient

def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightMap line 21
Source documentation
The same adjoint diagonal on the entire complexification.
```
def complexWeightMap : (ℂ ⊗[ℝ] L) →ₗ[ℂ] (Fin n → ℂ) where
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightMap_one_tmul line 30
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightMap_eq_zero_iff line 33
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightMap_root_zero line 60
Source documentation
The nonzero Cartan root spaces lie in the common complex weight kernel.
```
theorem complexWeightMap_root_zero
    {χ : complexifiedSubalgebra L H → ℂ} (hχ : χ ≠ 0)
    {x : ℂ ⊗[ℝ] L} (hx : x ∈ rootSpace (complexifiedSubalgebra L H) χ) :
    T.complexWeightMap x = 0 :=
…
```
Mentions: OAI.PolycyclicRecognition.complexifiedSubalgebra
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.exists_complex_cartan_representative line 69
Source documentation
All the complex weight coordinates have a common representative in the complexified Cartan subalgebra.
```
theorem exists_complex_cartan_representative (x : ℂ ⊗[ℝ] L) :
    ∃ h : complexifiedSubalgebra L H, T.complexWeightMap h = T.complexWeightMap x := by
…
```
Mentions: OAI.PolycyclicRecognition.complexifiedSubalgebra
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightMap_torusOperator line 90
Source documentation
Every element of the compact rotation group fixes the whole complex adjoint-weight quotient, not merely its kernel.
```
theorem complexWeightMap_torusOperator
    (z : complexCartanTorus L H) (x : ℂ ⊗[ℝ] L) :
    T.complexWeightMap (ComplexCartan.torusOperator (complexifiedSubalgebra L H) z.val x) =
      T.complexWeightMap x := by
…
```
Mentions: OAI.PolycyclicRecognition.complexCartanTorus, OAI.PolycyclicRecognition.ComplexCartan.torusOperator, OAI.PolycyclicRecognition.complexifiedSubalgebra
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightMap_realTorusOperator line 111
Source documentation
The real compact rotation action fixes the actual real weight quotient.
```
theorem weightMap_realTorusOperator (z : realRotationTorus L H) (x : L) :
    T.weightMap (realTorusOperator L H z x) = T.weightMap x := by
…
```
Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.realTorusOperator