OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationFactorKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent factor remains the kernel of the weight character

  1. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.weightCharacter_inclusionN line 23
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.inclusionN_range_eq_weightKernel line 28
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.weightCharacter_invariant_rotation line 53
  4. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationWeightCharacter line 62

    Source documentation

    The full vector-valued character survives the modification.

    def rotationWeightCharacter :
    F.SmoothRotationalModification hExp →* Multiplicative T.weightMap.range :=
…
  5. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationWeightCharacter_kernel line 68
  6. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.normal_nilpotentFactorToRotation line 85

    Source documentation

    Normality now follows from an actual homomorphism kernel.

    theorem normal_nilpotentFactorToRotation :
    (F.nilpotentFactorToRotation hExp).range.Normal := by
…