ComplexAdjointWeights.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Complex adjoint weights for solvable real Lie algebras

The existing simultaneous-basis construction applies over the complex numbers as well. Its restriction to real vectors supplies the weights whose lifted group characters are used in the general solvable lattice argument.

def OAI.PolycyclicRecognition.complexificationLieHom line 26
Source documentation
The canonical real Lie homomorphism into the complexification.
```
def complexificationLieHom : L →ₗ⁅ℝ⁆ ℂ ⊗[ℝ] L :=
…
```
theorem OAI.PolycyclicRecognition.complexificationLieHom_injective line 33

theorem OAI.PolycyclicRecognition.exists_complex_triangular_adjoint_basis line 41

Source documentation

A complex triangular basis of the actual complexified adjoint action.

theorem exists_complex_triangular_adjoint_basis [FiniteDimensional ℝ L]
    [LieAlgebra.IsSolvable L] :
    ∃ (n : ℕ) (b : Basis (Fin n) ℂ (ℂ ⊗[ℝ] L)),
      ∀ x : ℂ ⊗[ℝ] L,
        (LinearMap.toMatrix b b (LieAlgebra.ad ℂ (ℂ ⊗[ℝ] L) x)).IsUpperTriangular := by
…

def OAI.PolycyclicRecognition.complexifiedAdjointMatrix line 49
Source documentation
The complexified adjoint matrices, restricted to the original real algebra.
```
def complexifiedAdjointMatrix {n : ℕ} (b : Basis (Fin n) ℂ (ℂ ⊗[ℝ] L)) :
    L →ₗ⁅ℝ⁆ Matrix (Fin n) (Fin n) ℂ := by
…
```
theorem OAI.PolycyclicRecognition.complexifiedAdjointMatrix_apply line 58