CartanJordanDecomposition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Identifying the Cartan weight operator as the semisimple part

The polynomial Jordan decomposition shows that the weight operator preserves every subspace preserved by the original adjoint operator. This will keep the original triangular flag when the weight operator is subtracted.

theorem OAI.PolycyclicRecognition.cartanWeightOperator_jordan line 23
theorem OAI.PolycyclicRecognition.cartanWeightOperator_upper line 46
theorem OAI.PolycyclicRecognition.heightReducedAdjoint_nilpotent line 59
Source documentation
Removing the semisimple height action leaves a strictly triangular operator in the original adjoint flag.
```
theorem heightReducedAdjoint_nilpotent (x : L) :
    IsNilpotent (ad ℝ L x - (heightSemisimpleAction T H x).toLinearMap) := by
…
```
Mentions: OAI.PolycyclicRecognition.heightSemisimpleAction