BlockRootGroup.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The group generated by the roots within each block

The finite-orbit fixed-vector obstruction excludes singleton blocks. Without singleton blocks, the full matrix commutant of the root-generated group is exactly the block-scalar algebra. Its full normalizer therefore lies in the scalar-algebra normalizer used in orbit reduction.

def OAI.DukePrimeDegree.blockRootGroup line 22
lemma OAI.DukePrimeDegree.root_mem_blockRootGroup line 26
def OAI.DukePrimeDegree.rowVectorStabilizer line 31
lemma OAI.DukePrimeDegree.singleton_fixed_by_blockRootGroup line 45

theorem OAI.DukePrimeDegree.no_singleton_block_of_generic_finite_root_orbit line 62

Source documentation

A generic finite-volume root-group orbit has no singleton block.

theorem no_singleton_block_of_generic_finite_root_orbit {n : ℕ}
    (g : G n) (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (r : Setoid (Fin n)) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (μ : Measure (LatticeOrbitQuotient g (blockRootGroup r))) [IsFiniteMeasure μ]
    (hμ : μ ≠ 0)
    (hinv : ∀ h : blockRootGroup r,
      μ.map (fun x => latticeOrbitRightAction g (blockRootGroup r) x h) = μ) :
    ∀ k, ∃ j, k ≠ j ∧ r k j := by
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.blockRootGroup, OAI.DukePrimeDegree.latticeOrbitRightAction

lemma OAI.DukePrimeDegree.diagonal_commute_transvection_of_eq line 83
lemma OAI.DukePrimeDegree.blockRootGroup_le_blockMatrixGroup line 101

theorem OAI.DukePrimeDegree.blockScalar_mem_iff_commute_blockRoots line 111

Source documentation

Once singleton blocks are excluded, roots alone determine the full block-scalar commutant; no split diagonal is an extra hypothesis.

theorem blockScalar_mem_iff_commute_blockRoots {n : ℕ}
    (r : Setoid (Fin n)) (hnosingle : ∀ i, ∃ j, i ≠ j ∧ r i j)
    (M : Matrix (Fin n) (Fin n) ℝ) :
    M ∈ blockScalarAlgebra r ↔ ∀ i j, i ≠ j → r i j →
      Commute M (Matrix.transvection i j (1 : ℝ)) := by
…

Mentions: OAI.DukePrimeDegree.blockScalarAlgebra

theorem OAI.DukePrimeDegree.blockScalar_mem_iff_commute_blockRootGroup line 142
lemma OAI.DukePrimeDegree.conjugate_blockScalar_mem_of_root_normalizer line 157
theorem OAI.DukePrimeDegree.blockRootGroup_normalizer_le_scalarNormalizer line 179
Source documentation
The full root-group normalizer is contained in the already computed block-scalar normalizer, once finite-orbit recurrence removes singleton blocks.
```
theorem blockRootGroup_normalizer_le_scalarNormalizer {n : ℕ}
    (r : Setoid (Fin n)) (hnosingle : ∀ i, ∃ j, i ≠ j ∧ r i j) :
    Subgroup.normalizer (blockRootGroup r : Set (G n)) ≤ blockScalarNormalizer r := by
…
```
Mentions: OAI.DukePrimeDegree.blockRootGroup, OAI.DukePrimeDegree.blockScalarNormalizer