OAI/GroupTheory/PolycyclicRecognition/Geometry/RealRotationTorus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A compact torus of automorphisms preserving the real form

Commuting with the canonical conjugation is a closed subgroup condition. The resulting compact subgroup contains every real Cartan rotation.

  1. abbrev OAI.PolycyclicRecognition.complexCartanTorus line 20
  2. def OAI.PolycyclicRecognition.realRotationTorus line 24

    Source documentation

    Those compact diagonal automorphisms which preserve the original real Lie algebra, expressed by commutation with conjugation.

    def realRotationTorus : Subgroup (complexCartanTorus L H) where
…

    Mentions: OAI.PolycyclicRecognition.complexCartanTorus

  3. theorem OAI.PolycyclicRecognition.realRotationTorus_isClosed line 59

    Source documentation

    Conjugation commutation cuts out a closed subgroup of the compact torus.

    theorem realRotationTorus_isClosed : IsClosed (realRotationTorus L H : Set (complexCartanTorus L H)) := by
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus, OAI.PolycyclicRecognition.complexCartanTorus

  4. instance OAI.PolycyclicRecognition.realRotationTorus_compactSpace line 76
  5. def OAI.PolycyclicRecognition.realPhaseVector line 83

    Source documentation

    The genuine rotations by real Cartan parameters lie in the compact subgroup preserving the real form.

    def realPhaseVector (h : H) : realRotationTorus L H := by
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus