OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockIndexTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transport of the two-block chart to the arithmetic matrix group

The partition is the actual partition induced by a chosen enumeration of two coordinate blocks. Reindexing identifies its block matrix subgroup with the concrete neutral subgroup used in the parabolic chart.

  1. def OAI.DukePrimeDegree.twoBlockIndexSetoid line 21
  2. def OAI.DukePrimeDegree.twoBlockReindex line 25
  3. def OAI.DukePrimeDegree.twoBlockReindexHomeomorph line 44
  4. theorem OAI.DukePrimeDegree.reindex_cross_blocks_zero_iff line 58
  5. theorem OAI.DukePrimeDegree.twoBlockReindex_mem_neutral_iff line 97
  6. def OAI.DukePrimeDegree.twoBlockNeutralIndexEquiv line 108
  7. def OAI.DukePrimeDegree.twoBlockNeutralIndexHomeomorph line 118