OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereFreeness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Freeness of the shearing horosphere

A lattice with no nonzero vector on a coordinate hyperplane has no nonidentity stabilizer fixing a coordinate column. Root-horospherical matrices fix such a column. Full diagonal invariance gives the required lattice property almost everywhere, removing any small-size restriction from the compact shearing contradiction.

  1. lemma OAI.DukePrimeDegree.vecMul_fixed_column line 23
  2. theorem OAI.DukePrimeDegree.stabilizer_eq_one_of_fixed_column line 34
  3. theorem OAI.DukePrimeDegree.rootHorosphere_stabilizer_eq_one line 63
  4. theorem OAI.DukePrimeDegree.ae_rootHorosphere_stabilizer_trivial line 72