OAI/GroupTheory/PolycyclicRecognition/Geometry/IntegratedNilradicalRotations.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The compact rotations on the closed nilpotent factor

  1. def OAI.PolycyclicRecognition.modelNilradicalRotation line 19

    Source documentation

    The compact rotation on the chosen nilpotent model's tangent algebra.

    def modelNilradicalRotation (z : realRotationTorus L H) :
    GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier ≃ₗ⁅ℝ⁆
      GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier :=
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  2. theorem OAI.PolycyclicRecognition.modelNilradicalRotation_apply line 24
  3. theorem OAI.PolycyclicRecognition.modelNilradicalRotation_one line 29
  4. theorem OAI.PolycyclicRecognition.modelNilradicalRotation_mul line 37
  5. def OAI.PolycyclicRecognition.modelNilradicalLinearAction line 48

    Source documentation

    The transported linear representation.

    def modelNilradicalLinearAction : realRotationTorus L H →*
    (GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier ≃ₗ[ℝ]
      GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier) where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  6. theorem OAI.PolycyclicRecognition.modelNilradicalLinearAction_apply line 55
  7. theorem OAI.PolycyclicRecognition.continuous_modelNilradicalRotation line 65
  8. theorem OAI.PolycyclicRecognition.exists_integrated_nilradical_rotations line 79
  9. def OAI.PolycyclicRecognition.nilradicalRotations line 98

    Source documentation

    A fixed choice of the integrated compact action.

    def nilradicalRotations
    (Exp : GroupLieAlgebra (𝓘(ℝ,N.modelSpace)) N.carrier → N.carrier)
    (hExp : IsGroupExponential Exp) : realRotationTorus L H →* MulAut N.carrier :=
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  10. theorem OAI.PolycyclicRecognition.continuous_nilradicalRotations line 103
  11. theorem OAI.PolycyclicRecognition.nilradicalRotations_exp line 110