ComplexNilradical.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic meaning of the complex weight kernel

The common kernel consists exactly of the elements with nilpotent adjoint. In particular it is preserved by every Lie automorphism. This identifies the nilpotent factor without making a choice of triangular basis part of its data.

theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.diagonal_mul line 24
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.diagonal_pow line 35
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complex_ad_nilpotent line 44
Source documentation
Nilpotence of the real adjoint remains nilpotence after scalar extension.
```
theorem complex_ad_nilpotent (x : L) (hx : IsNilpotent (LieAlgebra.ad ℝ L x)) :
    IsNilpotent (LieAlgebra.ad ℂ (ℂ ⊗[ℝ] L) (complexificationLieHom L x)) := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationLieHom
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.mem_kernelIdeal_iff_ad_nilpotent line 70
Source documentation
The nilpotent kernel is independent of the chosen complex triangular basis.
```
theorem mem_kernelIdeal_iff_ad_nilpotent (x : L) :
    x ∈ T.kernelIdeal ↔ IsNilpotent (LieAlgebra.ad ℝ L x) := by
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.map_mem_kernelIdeal line 88
Source documentation
Every Lie automorphism preserves this concrete nilpotent ideal.
```
theorem map_mem_kernelIdeal (f : L ≃ₗ⁅ℝ⁆ L) {x : L} (hx : x ∈ T.kernelIdeal) :
    f x ∈ T.kernelIdeal := by
…
```