OAI/GroupTheory/PolycyclicRecognition/Geometry/ComplexAdjointGroup.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Additive complex adjoint weights on a simply connected solvable group

  1. theorem OAI.PolycyclicRecognition.complexAdjointMatrixHom_upper line 21

    Source documentation

    The triangular infinitesimal adjoint action exponentiates to a triangular group action, using only local exponential generation.

    theorem complexAdjointMatrixHom_upper
    (b : Basis (Fin m) ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (T : ComplexTriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) n)
    {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
    (g : G) : (complexAdjointMatrixHom b T.basis g).IsUpperTriangular := by
…

    Mentions: OAI.PolycyclicRecognition.ComplexTriangularAdjoint, OAI.PolycyclicRecognition.complexAdjointMatrixHom

  2. theorem OAI.PolycyclicRecognition.exists_additive_complex_adjoint_weights line 59