OAI/NumberTheory/DukePrimeDegree/Geometry/RowRootChart.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous coordinates for a full row of roots

The expanding group for a canonical diagonal flow is a full row (or, after transposition, a column). A nonzero pivot provides a global chart separating all its root coordinates simultaneously. This constructs the ambient chart needed for the abelian case of the product theorem.

  1. def OAI.DukePrimeDegree.rowTimeSpace line 21
  2. abbrev OAI.DukePrimeDegree.RowTime line 24
  3. lemma OAI.DukePrimeDegree.rowTime_self line 26
  4. def OAI.DukePrimeDegree.rowRoot line 28
  5. lemma OAI.DukePrimeDegree.mul_rowRoot_entry line 31
  6. lemma OAI.DukePrimeDegree.rowRoot_add line 37
  7. lemma OAI.DukePrimeDegree.rowRoot_zero line 51
  8. lemma OAI.DukePrimeDegree.continuous_rowRoot line 56
  9. abbrev OAI.DukePrimeDegree.RowRootSlice line 68
  10. def OAI.DukePrimeDegree.rowRootParameter line 71
  11. def OAI.DukePrimeDegree.rowPivotTranslate line 76
  12. lemma OAI.DukePrimeDegree.rowRootParameter_translate line 80
  13. def OAI.DukePrimeDegree.rowSliceRepresentative line 93
  14. lemma OAI.DukePrimeDegree.rowSliceRepresentative_translate line 106
  15. lemma OAI.DukePrimeDegree.continuous_rowRootParameter line 117
  16. lemma OAI.DukePrimeDegree.continuous_rowSliceRepresentative line 127
  17. def OAI.DukePrimeDegree.rowPivotHomeomorph line 133