OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanWeightDerivation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The semisimple derivations attached to canonical height

On a generalized Cartan root space the operator is scalar multiplication by the root. Its dependence on the canonical height, rather than a choice of Cartan representative, is proved here.

  1. def OAI.PolycyclicRecognition.cartanWeightOperator line 23
  2. theorem OAI.PolycyclicRecognition.cartanWeightOperator_apply_root line 29
  3. theorem OAI.PolycyclicRecognition.cartanWeightOperator_apply_genWeight line 42
  4. theorem OAI.PolycyclicRecognition.cartanWeightOperator_lie line 49
  5. def OAI.PolycyclicRecognition.cartanWeightDerivation line 70
  6. theorem OAI.PolycyclicRecognition.cartanWeightDerivation_apply_root line 78
  7. theorem OAI.PolycyclicRecognition.cartanWeightDerivation_add line 82
  8. theorem OAI.PolycyclicRecognition.cartanWeightDerivation_smul line 96
  9. def OAI.PolycyclicRecognition.cartanWeightDerivationLinear line 109
  10. theorem OAI.PolycyclicRecognition.cartanWeightDerivation_commute line 114
  11. def OAI.PolycyclicRecognition.heightSemisimpleAction line 132

    Source documentation

    The chosen Cartan section disappears from the eigenvalues: they are the canonical height weights.

    def heightSemisimpleAction : L →ₗ[ℝ] LieDerivation ℝ L L :=
…
  12. theorem OAI.PolycyclicRecognition.heightSemisimpleAction_apply_root line 136
  13. theorem OAI.PolycyclicRecognition.heightSemisimpleAction_lie line 142
  14. theorem OAI.PolycyclicRecognition.heightSemisimpleAction_commute line 148
  15. theorem OAI.PolycyclicRecognition.heightSemisimpleAction_height_zero line 152
  16. theorem OAI.PolycyclicRecognition.heightSemisimpleAction_annihilate line 170