OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootLongBoxes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Long boxes for the full positive-root group

The ordered root word is injective. Generic arithmetic lattices have free upper unipotent orbits, so every compact set of full root times fits into one actual quotient box containing the chosen basepoint.

  1. lemma OAI.DukePrimeDegree.allPositiveRoots_closed line 21
  2. theorem OAI.DukePrimeDegree.ae_upperRoot_stabilizer_trivial line 28
  3. theorem OAI.DukePrimeDegree.upperRootWord_injective line 37
  4. lemma OAI.DukePrimeDegree.upperRootQuotientParam_zero line 44
  5. theorem OAI.DukePrimeDegree.upperRootQuotientParam_injective_of_free line 49
  6. theorem OAI.DukePrimeDegree.upperRootBox_contains_compact_time line 72
  7. theorem OAI.DukePrimeDegree.upperRootBox_arbitrary_compact_of_free line 93