OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootGlobalCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Global coordinates on the upper unipotent group

Gaussian elimination never encounters a zero pivot on a unipotent upper triangular matrix. Consequently the ordered root word covers that entire group, and is a homeomorphism onto it.

  1. lemma OAI.DukePrimeDegree.upperRoot_diagonal line 20
  2. lemma OAI.DukePrimeDegree.upperRoot_zeroPattern_eq_one line 27
  3. theorem OAI.DukePrimeDegree.EliminationChain.exists_param_of_upperRoot line 41
  4. theorem OAI.DukePrimeDegree.upperRootWord_surjective line 67
  5. def OAI.DukePrimeDegree.upperRootWordMap line 81
  6. theorem OAI.DukePrimeDegree.upperRootWordMap_bijective line 85
  7. theorem OAI.DukePrimeDegree.upperRootWord_isEmbedding line 93
  8. theorem OAI.DukePrimeDegree.upperRootWordMap_isEmbedding line 102
  9. def OAI.DukePrimeDegree.upperRootWordHomeomorph line 105
  10. lemma OAI.DukePrimeDegree.upperRootWordHomeomorph_apply line 109