RootOrbitRationality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Prime-degree obstruction for finite root-group orbits

Polynomial recurrence replaces the full diagonal subgroup in the matrix density argument. The result applies to any finite-volume orbit group L that contains the block roots and preserves the blocks. For the root- generated group itself, fixed-vector recurrence first excludes singletons. No finite-volume-orbit existence assertion is assumed or proved here.

theorem OAI.DukePrimeDegree.centralizer_subset_blockScalar_of_finite_root_orbit line 23
theorem OAI.DukePrimeDegree.rationalBlockRealSpan_of_centralizer_image line 67

theorem OAI.DukePrimeDegree.root_partition_universal_of_finite_root_containing_orbit line 133

Source documentation

This applies to the actual larger orbit group L, provided it contains the non-singleton block roots and preserves the blocks.

theorem root_partition_universal_of_finite_root_containing_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)
    (hnosingle : ∀ 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_finite_blockRoot_orbit line 152

Source documentation

A generic finite-volume orbit of the nontrivial root-generated group in prime degree already forces the root partition to be universal.

theorem root_partition_universal_of_generic_finite_blockRoot_orbit {n : ℕ}
    (hn : n.Prime) (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) = μ) :
    ∀ i j, r i j := by
…

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