OAI/GroupTheory/PolycyclicRecognition/Geometry/NilradicalRotationAction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The compact rotation action on the actual nilpotent kernel

  1. def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.nilradicalRotation line 18

    Source documentation

    Restrict the real rotations to the intrinsic nilpotent adjoint kernel.

    def nilradicalRotation (z : realRotationTorus L H) : T.kernelIdeal ≃ₗ⁅ℝ⁆ T.kernelIdeal where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  2. def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.nilradicalLinearAction line 37

    Source documentation

    The restricted linear representation has the same compact parameter group.

    def nilradicalLinearAction : realRotationTorus L H →* (T.kernelIdeal ≃ₗ[ℝ] T.kernelIdeal) where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  3. theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.continuous_nilradicalRotation line 49