BlockOrbit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The standard block group and its finite-volume lattice orbits

The group here is defined by its concrete action on the coordinate blocks. The split diagonals and all within-block root groups lie in it. The preceding rationality argument then forces any nontrivial partition with a finite-volume orbit through a generic prime-degree lattice to be the universal partition.

def OAI.DukePrimeDegree.blockMatrixGroup line 25
Source documentation
The determinant-one matrices commuting with every block-scalar diagonal. This is the usual block-diagonal matrix subgroup.
```
def blockMatrixGroup {n : ℕ} (r : Setoid (Fin n)) : Subgroup (G n) where
…
```
lemma OAI.DukePrimeDegree.blockMatrixGroup_commute line 40
lemma OAI.DukePrimeDegree.diagonalOneParameter_mem_blockMatrixGroup line 50
lemma OAI.DukePrimeDegree.transvection_mem_blockMatrixGroup line 57

theorem OAI.DukePrimeDegree.block_partition_universal_of_finite_orbit line 67

Source documentation

A generic lattice in prime dimension has no finite-volume orbit under a proper nontrivial block group. All matrix-group and rationality conditions have been discharged for this concrete block subgroup.

theorem block_partition_universal_of_finite_orbit {d : ℕ}
    (hn : (d + 1).Prime) (g : G (d + 1))
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (r : Setoid (Fin (d + 1))) (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (μ : Measure (LatticeOrbitQuotient g (blockMatrixGroup r)))
    [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : blockMatrixGroup r,
      μ.map (fun x => latticeOrbitRightAction g (blockMatrixGroup r) x h) = μ) :
    ∀ i j, r i j := by
…

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