OAI/GroupTheory/PolycyclicRecognition/Geometry/RepresentationKernelAdjoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.adjointLinearMap_eq_id_of_representation_kernel line 18
2. theorem OAI.PolycyclicRecognition.lieHom_adjoint_of_exponential_intertwining line 51

   Source documentation

   Exponential compatibility also intertwines the full adjoint action.

   theorem lieHom_adjoint_of_exponential_intertwining
       {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
       (j : GroupLieAlgebra (𝓘(ℝ, E)) G →ₗ⁅ℝ⁆ A)
       (ρ : G →* Aˣ) (he : ∀ x, ρ (Exp x) = algebraExpUnit (j x))
       (g : G) (x : GroupLieAlgebra (𝓘(ℝ, E)) G) :
       j (adjointLinearMap (E := E) g x) = (ρ g : A) * j x * (ρ g)⁻¹ := by
   …

   Mentions: OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.adjointLinearMap