OAI/GroupTheory/PolycyclicRecognition/Algebra/RealTorusAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The compact rotational group acts on the real Lie algebra

  1. def OAI.PolycyclicRecognition.realTorusOperator line 17

    Source documentation

    The compact torus action restricted to the original real form.

    def realTorusOperator (z : realRotationTorus L H) : L →ₗ[ℝ] L :=
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  2. theorem OAI.PolycyclicRecognition.realTorusOperator_complexify line 22
  3. theorem OAI.PolycyclicRecognition.realTorusOperator_one line 35
  4. theorem OAI.PolycyclicRecognition.realTorusOperator_mul line 41
  5. theorem OAI.PolycyclicRecognition.realTorusOperator_lie line 48
  6. def OAI.PolycyclicRecognition.realTorusAutomorphism line 58

    Source documentation

    Actual real Lie automorphisms, indexed by the compact torus.

    def realTorusAutomorphism (z : realRotationTorus L H) : L ≃ₗ⁅ℝ⁆ L where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  7. def OAI.PolycyclicRecognition.realTorusLinearAction line 68

    Source documentation

    The underlying linear representation of the compact group.

    def realTorusLinearAction : realRotationTorus L H →* (L ≃ₗ[ℝ] L) where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus