OAI/GroupTheory/PolycyclicRecognition/Geometry/IntrinsicAdjointHeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic adjoint height on a connected triangular Lie group

The actual adjoint action is positive upper triangular because this holds on exponential basis curves, which generate the connected group. Its logarithmic diagonal is therefore a continuous character without a global exponential chart or a faithful group representation.

  1. theorem OAI.PolycyclicRecognition.adjointMatrixHom_exp_intrinsic line 24
  2. theorem OAI.PolycyclicRecognition.continuous_adjointMatrixHom line 44
  3. theorem OAI.PolycyclicRecognition.adjointMatrixHom_positive_triangular line 54
  4. def OAI.PolycyclicRecognition.intrinsicAdjointCharacterHom line 79

    Source documentation

    The character is constructed from the actual adjoint action.

    def intrinsicAdjointCharacterHom {n : ℕ}
    (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) n)
    {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp) :
    G →* Multiplicative (Fin n → ℝ) :=
…

    Mentions: OAI.PolycyclicRecognition.TriangularAdjoint

  5. theorem OAI.PolycyclicRecognition.intrinsicAdjointCharacterHom_exp line 87
  6. theorem OAI.PolycyclicRecognition.continuous_intrinsicAdjointCharacterHom line 96