OAI/NumberTheory/DukePrimeDegree/Dynamics/BlockNormalizerFiniteIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The finite quotient of the block normalizer

Conjugation acts on the finite set of idempotents in the block-scalar algebra. The kernel is precisely the block matrix group. Thus the latter has finite index in the full normalizer, including its disconnected part.

  1. def OAI.DukePrimeDegree.BlockIdempotent line 23
  2. lemma OAI.DukePrimeDegree.blockIdempotent_diagonal line 26
  3. lemma OAI.DukePrimeDegree.blockIdempotent_entry_zero_or_one line 30
  4. instance OAI.DukePrimeDegree.blockIdempotentFinite line 38
  5. lemma OAI.DukePrimeDegree.slMatrixConjugation_eq_self_of_mem_blockMatrixGroup line 51
  6. lemma OAI.DukePrimeDegree.blockMatrixGroup_le_scalarNormalizer line 59
  7. lemma OAI.DukePrimeDegree.mem_blockMatrixGroup_of_fixes_blockProjection line 72
  8. def OAI.DukePrimeDegree.blockIdempotentConjugate line 93
  9. instance OAI.DukePrimeDegree.blockIdempotentMulAction line 102
  10. def OAI.DukePrimeDegree.blockNormalizerPermutation line 115
  11. lemma OAI.DukePrimeDegree.blockNormalizerPermutation_ker line 119
  12. theorem OAI.DukePrimeDegree.blockMatrixGroup_finiteIndex_in_scalarNormalizer line 142

    Source documentation

    Only finitely many block-group cosets occur in the full algebra normalizer.

    theorem blockMatrixGroup_finiteIndex_in_scalarNormalizer {n : ℕ} (r : Setoid (Fin n)) :
    ((blockMatrixGroup r).comap (blockScalarNormalizer r).subtype).FiniteIndex := by
…

    Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.blockScalarNormalizer

  13. theorem OAI.DukePrimeDegree.finite_blockNormalizer_quotient line 147