NeutralBlockLocalInvariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local invariance under the full neutral block group

Within-block root invariance and full diagonal invariance suffice for invariance under a neighborhood of the identity in the block group. The proof uses the already constructed finite Gaussian elimination: a small block matrix outside the subgroup would normalize to a positive scalar determinant-one matrix still outside it, which is impossible. Disconnected block components are not asserted to preserve the measure.

theorem OAI.DukePrimeDegree.block_subgroup_mem_nhds_of_roots_and_diagonals line 26

theorem OAI.DukePrimeDegree.open_block_stabilizer_of_roots_and_diagonals line 79

Source documentation

The actual stabilizer contains an open subgroup of the neutral block group. This is the form needed for a local neutral product chart.

theorem open_block_stabilizer_of_roots_and_diagonals {n : ℕ}
    (hn : n ≠ 0) (r : Setoid (Fin n)) (μ : Measure (X n))
    (hroot : ∀ (i j : Fin n) (hij : i ≠ j), r i j → ∀ t : ℝ,
      μ.map (fun x => rightAction x (SpecialLinearGroup.transvection hij t)) = μ)
    (hdiag : ∀ (v : Fin n → ℝ) (hv : ∑ i, v i = 0) (t : ℝ),
      μ.map (fun x => rightAction x (diagonalOneParameter v hv t)) = μ) :
    IsOpen (((invariantRightSubgroup μ).comap (blockMatrixGroup r).subtype :
      Subgroup (blockMatrixGroup r)) : Set (blockMatrixGroup r)) :=
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup