OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationFactorLifts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The original nilpotent factors inside the actual rotational graph

  1. theorem OAI.PolycyclicRecognition.rotation_inv_apply_of_eq_one line 13
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationCharacter_inclusionN line 32
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.inverse_rotation_fixes_nilpotent_factor line 37
  4. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.inverse_rotation_fixes_cartan_factor line 43
  5. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.nilpotentFactorToRotation line 50

    Source documentation

    The actual nilpotent kernel embeds with its original multiplication.

    def nilpotentFactorToRotation : F.N.carrier →* F.SmoothRotationalModification hExp :=
…
  6. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.cartanFactorToRotation line 56

    Source documentation

    The Cartan factor also retains its original multiplication.

    def cartanFactorToRotation : F.D.carrier →* F.SmoothRotationalModification hExp :=
…
  7. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_nilpotentFactorToRotation line 61
  8. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_cartanFactorToRotation line 66