OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootChart.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Actual charts for the full upper unipotent group

The complete Gaussian elimination chain supplies an open group chart. Left translation and the discrete lattice covering then give local product charts in the arithmetic quotient around every point. Every time factor is an actual ordered product of positive-root matrices.

  1. def OAI.DukePrimeDegree.completeRootChain line 21
  2. lemma OAI.DukePrimeDegree.completeRootChain_final line 24
  3. abbrev OAI.DukePrimeDegree.UpperRootTransverse line 27
  4. abbrev OAI.DukePrimeDegree.UpperRootTime line 28
  5. def OAI.DukePrimeDegree.emptyEliminationHomeomorph line 30
  6. def OAI.DukePrimeDegree.upperRootParam line 39
  7. theorem OAI.DukePrimeDegree.upperRootParam_isOpenEmbedding line 42
  8. lemma OAI.DukePrimeDegree.upperRootParam_eq_mul line 47
  9. lemma OAI.DukePrimeDegree.upperRootWord_mem line 51
  10. def OAI.DukePrimeDegree.upperRootIdentity line 56
  11. lemma OAI.DukePrimeDegree.upperRootParam_zero line 68
  12. def OAI.DukePrimeDegree.upperRootQuotientParam line 72
  13. theorem OAI.DukePrimeDegree.upperRootQuotientParam_localHomeomorph line 76
  14. lemma OAI.DukePrimeDegree.upperRootQuotientParam_eq_action line 82
  15. structure OAI.DukePrimeDegree.UpperRootBox line 90
  16. theorem OAI.DukePrimeDegree.exists_upperRootBox_at_coordinates line 98
  17. theorem OAI.DukePrimeDegree.exists_upperRootBox_at line 108