WeightRotationDerivation.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The infinitesimal rotation factors through the complex weight quotient

theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.realImaginaryOperator_eq_zero line 20
Source documentation
No infinitesimal rotation remains on a nilpotent Cartan parameter.
```
theorem realImaginaryOperator_eq_zero (h : H) (hh : T.weightMap (h : L) = 0) (x : L) :
    realImaginaryOperator L H h x = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.realImaginaryOperator
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.realImaginaryOperator_eq_of_weightMap_eq line 37
def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightImaginaryAction line 49
Source documentation
The infinitesimal imaginary action depends only on the actual weight quotient; this is the derivative used in the rotational modification.
```
def weightImaginaryAction : L →ₗ[ℝ] LieDerivation ℝ L L :=
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightImaginaryAction_cartan line 53
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightImaginaryAction_kernel line 58
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightImaginaryAction_lie line 65
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightMap_realImaginaryOperator line 70
Source documentation
The infinitesimal rotation acts trivially on the whole weight quotient.
```
theorem weightMap_realImaginaryOperator (h : H) (x : L) :
    T.weightMap (realImaginaryOperator L H h x) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.realImaginaryOperator
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightImaginaryAction_annihilate line 87
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightImaginaryAction_commute line 93
Source documentation
The quotient derivations commute.
```
theorem weightImaginaryAction_commute (x y : L) :
    ⁅T.weightImaginaryAction H x,T.weightImaginaryAction H y⁆ = 0 := by
…
```