OAI/GroupTheory/PolycyclicRecognition/Geometry/FactorRotationCharacter.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The invariant compact character for the actual Cartan factors

  1. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationCharacter line 24

    Source comment

    The actual quotient character followed by its compact rotational part.
    def rotationCharacter : G →* realRotationTorus (GroupLieAlgebra (𝓘(ℝ,E)) G) H :=
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.continuous_rotationCharacter line 27
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationCharacter_exp line 30
  4. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationCharacter_cartan line 35
  5. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.weightCharacter_nilradical line 40
  6. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationCharacter_nilradical line 46
  7. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationCharacter_invariant line 51
  8. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.exists_invariant_compact_rotations line 65