GenericBlockOrbit.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Prime obstruction for the larger homogeneous orbit group

The actual finite-volume orbit group may strictly contain the group generated by the roots. Genericity and one root already force its stabilizer centralizer to be commutative. Thus block preservation is enough: no absence-of-singletons or split-diagonal hypothesis is needed.

lemma OAI.DukePrimeDegree.blockScalar_mem_of_commutes_roots_and_blocks line 22

theorem OAI.DukePrimeDegree.centralizer_subset_blockScalar_of_generic_finite_root_orbit line 48

Source documentation

The centralizer identification for the larger actual orbit group, including partitions having singleton blocks.

theorem centralizer_subset_blockScalar_of_generic_finite_root_orbit {n : ℕ}
    (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (L : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g L)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : L, μ.map (fun x => latticeOrbitRightAction g L x h) = μ)
    (r : Setoid (Fin n)) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (hblock : L ≤ blockMatrixGroup r)
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g L, Commute M s.val.val) :
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.pointOrbitStabilizer

theorem OAI.DukePrimeDegree.root_partition_universal_of_generic_finite_blockPreserving_orbit line 77

Source documentation

Prime-degree arithmetic applied directly to a finite-volume larger orbit group L. Only the concrete block-preserving inclusion remains; there is no separate finite-volume assumption on the root group.

theorem root_partition_universal_of_generic_finite_blockPreserving_orbit {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (L : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g L)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : L, μ.map (fun x => latticeOrbitRightAction g L x h) = μ)
    (r : Setoid (Fin n)) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (hblock : L ≤ blockMatrixGroup r) : ∀ i j, r i j := by
…

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

theorem OAI.DukePrimeDegree.root_partition_universal_of_generic_blockPreserving_orbit_measure line 95

Source documentation

The same conclusion with a finite invariant measure on the ambient lattice space concentrated on the actual L-orbit.

theorem root_partition_universal_of_generic_blockPreserving_orbit_measure {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (L : Subgroup (G n)) (hL : IsClosed (L : Set (G n)))
    (μ : Measure (X n)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (horbit : ∀ᵐ x ∂μ, x ∈ range (latticeOrbitPoint g L))
    (hinv : ∀ h : L, μ.map (fun x => rightAction x h.val) = μ)
    (r : Setoid (Fin n)) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (hblock : L ≤ blockMatrixGroup r) : ∀ i j, r i j := by
…

Mentions: OAI.DukePrimeDegree.latticeOrbitPoint, OAI.DukePrimeDegree.blockMatrixGroup