OAI/GroupTheory/PolycyclicRecognition/Geometry/AdjointMatrixHeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.matrixLogDiagonalHom line 14
2. theorem OAI.PolycyclicRecognition.matrixLogDiagonalHom_apply line 30
3. def OAI.PolycyclicRecognition.adjointMatrixHom line 38
4. theorem OAI.PolycyclicRecognition.adjointMatrixHom_exp line 47
5. theorem OAI.PolycyclicRecognition.adjointMatrixHom_upper line 58
6. theorem OAI.PolycyclicRecognition.adjointMatrixHom_exp_diagonal line 69
7. def OAI.PolycyclicRecognition.adjointCharacterHom line 81

   Source documentation

   The actual adjoint diagonal integrates exactly the canonical height characters, using the already required representation and exponential chart.

   def adjointCharacterHom {n : ℕ}
       (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) n)
       {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
       (hsurj : Function.Surjective Exp)
       (j : GroupLieAlgebra (𝓘(ℝ, E)) G →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ)
       (hρ : Function.Injective ρ) (hρExp : ∀ x, ρ (Exp x) = algebraExpUnit (j x)) :
       G →* Multiplicative (Fin n → ℝ) :=
   …

   Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.algebraExpUnit

8. theorem OAI.PolycyclicRecognition.adjointCharacterHom_exp line 96