OAI/NumberTheory/DukePrimeDegree/Geometry/WeylReindex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Permuting coordinates on the arithmetic quotient

Coordinate reversal transfers the increasing regular weight construction to its decreasing counterpart. Reindexing preserves determinant one and the integral lattice, so it acts on the actual quotient.

  1. def OAI.DukePrimeDegree.reindexSpecialLinear line 18
  2. lemma OAI.DukePrimeDegree.continuous_reindexSpecialLinear line 38
  3. lemma OAI.DukePrimeDegree.reindexSpecialLinear_integral line 45
  4. def OAI.DukePrimeDegree.quotientReindex line 53
  5. lemma OAI.DukePrimeDegree.quotientReindex_rightAction line 62
  6. lemma OAI.DukePrimeDegree.quotientReindex_symm_apply line 69
  7. lemma OAI.DukePrimeDegree.continuous_quotientReindex line 77
  8. def OAI.DukePrimeDegree.quotientReindexHomeomorph line 82