OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockTransverse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A single-block correction retains a transverse limiting shear

Only the selected block is normalized to a scalar. Its complement may have arbitrary entries. Conjugation by the selected root group fixes the entire block-diagonal part, so every nonidentity limiting shear is outside the two-block preserving group.

  1. def OAI.DukePrimeDegree.blockComplementSetoid line 22
  2. lemma OAI.DukePrimeDegree.singleBlockRootGroup_le_blockComplement line 26
  3. lemma OAI.DukePrimeDegree.matrix_commute_transvection_of_row_column line 34
  4. lemma OAI.DukePrimeDegree.withinBlockPart_singleBlock_commutes line 57
  5. theorem OAI.DukePrimeDegree.withinBlockPart_singleBlock_conjugation line 97
  6. theorem OAI.DukePrimeDegree.singleBlock_conjugation_limit_outside_blocks line 114