OAI/GroupTheory/PolycyclicRecognition/Geometry/RealShadowConjugation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The corrected Cartan action in a representation of the real shadow

  1. def OAI.PolycyclicRecognition.cartanAdjointCLM line 19
  2. def OAI.PolycyclicRecognition.cartanImaginaryCLM line 22
  3. theorem OAI.PolycyclicRecognition.cartan_correction_exp line 25
  4. theorem OAI.PolycyclicRecognition.realShadow_representation_corrected_action line 44

    Source documentation

    The original Cartan action followed by inverse rotation becomes ordinary matrix conjugation in every representation of the real-shadow algebra.

    theorem realShadow_representation_corrected_action
    (j : CartanRealShadow T H →ₗ⁅ℝ⁆ A) (h : H) (y : L) :
    j (cartanRealShadowEquiv T H
      ((NormedSpace.exp (-cartanImaginaryCLM H h))
        ((NormedSpace.exp (cartanAdjointCLM H h)) y))) =
      NormedSpace.exp (j (cartanRealShadowEquiv T H h)) *
        j (cartanRealShadowEquiv T H y) *
          NormedSpace.exp (-j (cartanRealShadowEquiv T H h)) := by
…

    Mentions: OAI.PolycyclicRecognition.CartanRealShadow, OAI.PolycyclicRecognition.cartanRealShadowEquiv, OAI.PolycyclicRecognition.cartanImaginaryCLM, OAI.PolycyclicRecognition.cartanAdjointCLM