BlockGroupNormalizer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Normalizers of the concrete block matrix group

The block-scalar algebra is the full matrix commutant of the block matrix group. Consequently a group normalizer preserves that algebra, and its identity component lies in the block matrix group itself.

lemma OAI.DukePrimeDegree.matrix_diagonal_of_commute_regular line 20
lemma OAI.DukePrimeDegree.blockScalar_mem_iff_commute_blockMatrixGroup line 37
lemma OAI.DukePrimeDegree.conjugate_blockScalar_mem_of_group_normalizer line 69
theorem OAI.DukePrimeDegree.blockMatrixGroup_normalizer_le_scalarNormalizer line 91
Source documentation
A normalizer of the block group also normalizes its full matrix commutant, which is the block-scalar algebra.
```
theorem blockMatrixGroup_normalizer_le_scalarNormalizer {d : ℕ}
    (r : Setoid (Fin (d + 1))) :
    Subgroup.normalizer (blockMatrixGroup r : Set (G (d + 1))) ≤ blockScalarNormalizer r := by
…
```
Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.blockScalarNormalizer

theorem OAI.DukePrimeDegree.connected_blockMatrixGroup_normalizer_le line 104

Source documentation

Every connected subgroup normalizing the concrete block group is already block diagonal.

theorem connected_blockMatrixGroup_normalizer_le {d : ℕ}
    (r : Setoid (Fin (d + 1))) (H : Subgroup (G (d + 1))) [PreconnectedSpace H]
    (hH : H ≤ Subgroup.normalizer (blockMatrixGroup r : Set (G (d + 1)))) :
    H ≤ blockMatrixGroup r := by
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup