ComplexAdjointKernel.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent kernel of the complex adjoint weights

Complex weights retain rotational directions. Their common real kernel is nilpotent by triangular matrices, faithful scalar extension, and Engel's theorem.

structure OAI.PolycyclicRecognition.ComplexTriangularAdjoint line 22
def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightMap line 30
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.mul_diag line 41
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightMap_lie line 52
def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.kernelIdeal line 62
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.mem_kernelIdeal line 66
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.matrix_nilpotent line 69
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.ad_nilpotent line 81
Source documentation
Vanishing complex weights force the original real adjoint operator to be nilpotent.
```
theorem ad_nilpotent (x : L) (hx : x ∈ T.kernelIdeal) :
    IsNilpotent (LieAlgebra.ad ℝ L x) := by
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.kernelIdeal_nilpotent line 105
Source documentation
The common kernel is a nilpotent Lie ideal, even when weights are nonreal.
```
theorem kernelIdeal_nilpotent [FiniteDimensional ℝ L] :
    LieRing.IsNilpotent T.kernelIdeal := by
…
```