OAI/GroupTheory/PolycyclicRecognition/Lattices/NilshadowHeight.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A fixed linear section of the nilshadow height

The section vectors are the logarithmic coordinates of the actual integral quotient lifts. The removed action fixes them, as well as the height map.

  1. def OAI.PolycyclicRecognition.IntegralNilshadowData.height line 18
  2. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.height_smooth line 21
  3. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.height_embed line 25
  4. def OAI.PolycyclicRecognition.IntegralNilshadowData.heightLinear line 29
  5. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.heightLinear_apply line 32
  6. def OAI.PolycyclicRecognition.IntegralNilshadowData.quotientBasis line 35
  7. def OAI.PolycyclicRecognition.IntegralNilshadowData.quotientSection line 37
  8. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.heightLinear_section line 41
  9. def OAI.PolycyclicRecognition.IntegralNilshadowData.completedLieAction line 51
  10. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.completedLieAction_height line 55
  11. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.completedLieAction_section line 66
  12. def OAI.PolycyclicRecognition.IntegralNilshadowData.heightProjection line 84
  13. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.heightLinear_projection line 87
  14. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.completedLieAction_projection line 91
  15. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.projection_completedLieAction line 95