OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Row and column coordinates for the shearing horosphere

Every element factors uniquely into a column displacement and a row displacement, with the shared root entry assigned to the row factor. The determinant lemma constructs both factors in the special linear group without extending the ambient group.

  1. def OAI.DukePrimeDegree.rootRowElement line 21
  2. def OAI.DukePrimeDegree.rootColumnElement line 26
  3. lemma OAI.DukePrimeDegree.rootRowElement_entry line 31
  4. lemma OAI.DukePrimeDegree.rootColumnElement_entry line 37
  5. theorem OAI.DukePrimeDegree.rootRowElement_shape line 43
  6. theorem OAI.DukePrimeDegree.rootColumnElement_shape line 53
  7. def OAI.DukePrimeDegree.horosphereRowCoordinates line 63
  8. def OAI.DukePrimeDegree.horosphereColumnCoordinates line 66
  9. lemma OAI.DukePrimeDegree.horosphereRowCoordinates_self line 69
  10. lemma OAI.DukePrimeDegree.horosphereColumnCoordinates_self line 73
  11. theorem OAI.DukePrimeDegree.rootHorosphere_column_row_factorization line 80
  12. theorem OAI.DukePrimeDegree.rootColumn_mul_rootRow_entry line 107