OrbitRationality.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Rational block centralizers from finite-volume lattice orbits

The rational matrices in the integral orbit-stabilizer centralizer span its real centralizer. Conjugation by the actual lattice matrix transports this statement to the embedding coordinates. Finite-orbit density then identifies this transported centralizer with the block-scalar algebra.

def OAI.DukePrimeDegree.slMatrixConjugationHom line 21
def OAI.DukePrimeDegree.slMatrixConjugationLinear line 34
lemma OAI.DukePrimeDegree.slMatrixConjugationLinear_apply line 38
lemma OAI.DukePrimeDegree.slMatrixConjugation_inverse line 42
lemma OAI.DukePrimeDegree.rationalMatrixCast_latticeStabilizer line 47
lemma OAI.DukePrimeDegree.pointOrbitStabilizer_eq_conjugate line 57
Source documentation
Every actual point stabilizer element is a conjugated integral stabilizer element. This uses the integral quotient, not an abstract field action.
```
lemma pointOrbitStabilizer_eq_conjugate {n : ℕ} (g : G n) (H : Subgroup (G n))
    (s : pointOrbitStabilizer g H) :
    ∃ γ : latticeOrbitStabilizer g H,
      slMatrixConjugation g (rationalMatrixCast (latticeStabilizerMatrix g H γ)) =
        s.val.val.val := by
…
```
Mentions: OAI.DukePrimeDegree.pointOrbitStabilizer, OAI.DukePrimeDegree.latticeOrbitStabilizer, OAI.DukePrimeDegree.slMatrixConjugation, OAI.DukePrimeDegree.rationalMatrixCast, OAI.DukePrimeDegree.latticeStabilizerMatrix
lemma OAI.DukePrimeDegree.conjugate_rational_commutant_mem_block line 77
lemma OAI.DukePrimeDegree.conjugate_rational_commutant_diagonal_mem line 97

theorem OAI.DukePrimeDegree.rationalBlockRealSpan_of_finite_orbit line 125

Source documentation

The real-span condition required by the prime-block endpoint follows from the finite volume of the actual block orbit. Both inclusions use the given matrix group; no rational field action is assumed.

theorem rationalBlockRealSpan_of_finite_orbit {n : ℕ}
    (g : G n) (H : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g H)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : H, μ.map (fun x => latticeOrbitRightAction g H x h) = μ)
    (ell : Fin n → ℝ) (hsum : ∑ i, ell i = 0) (hell : Function.Injective ell)
    (hdiag : ∀ t : ℝ, diagonalOneParameter ell hsum t ∈ H)
    (r : Setoid (Fin n))
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ H)
    (hblock : ∀ h : H, ∀ c ∈ blockCoordinateAlgebra r, Commute (Matrix.diagonal c) h.val.val)
    {c : Fin n → ℝ} (hc : c ∈ blockCoordinateAlgebra r) :
    c ∈ rationalBlockRealSpan g r := by
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.blockCoordinateAlgebra, OAI.DukePrimeDegree.rationalBlockRealSpan

theorem OAI.DukePrimeDegree.root_partition_universal_of_finite_orbit line 175

Source documentation

A nontrivial root block of a finite-volume block orbit in generic prime degree must contain every coordinate.

theorem root_partition_universal_of_finite_orbit {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (H : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g H)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : H, μ.map (fun x => latticeOrbitRightAction g H x h) = μ)
    (ell : Fin n → ℝ) (hsum : ∑ i, ell i = 0) (hell : Function.Injective ell)
    (hdiag : ∀ t : ℝ, diagonalOneParameter ell hsum t ∈ H)
    (r : Setoid (Fin n))
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ H)
    (hblock : ∀ h : H, ∀ c ∈ blockCoordinateAlgebra r, Commute (Matrix.diagonal c) h.val.val)
…

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