OAI/GroupTheory/PolycyclicRecognition/Geometry/RealTorusSmoothRepresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.realTorusUnitAction line 17

   Source documentation

   The compact rotations as units of the continuous endomorphism algebra.

   def realTorusUnitAction : realRotationTorus L H →* (L →L[ℝ] L)ˣ where
   …

   Mentions: OAI.PolycyclicRecognition.realRotationTorus

2. theorem OAI.PolycyclicRecognition.realTorusUnitAction_apply line 30
3. theorem OAI.PolycyclicRecognition.continuous_realTorusUnitAction line 33
4. theorem OAI.PolycyclicRecognition.contMDiff_realTorusRepresentation line 52

   Source documentation

   A continuous compact rotation character of a Lie group has a smooth linear representation. No manifold structure on the compact torus is needed.

   theorem contMDiff_realTorusRepresentation
       {Exp : GroupLieAlgebra (𝓘(ℝ,E)) G → G} (hExp : IsGroupExponential Exp)
       (q : G →* realRotationTorus L H) (hq : Continuous q) :
       ContMDiff (𝓘(ℝ,E)) (𝓘(ℝ,L →L[ℝ] L)) ∞
         (fun g => (realTorusUnitAction H (q g) : L →L[ℝ] L)) := by
   …

   Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.realTorusUnitAction