OAI/NumberTheory/DukePrimeDegree/Dynamics/NoFixedVectorOrbit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

No fixed coordinate subspace on a generic finite root orbit

The actual integral stabilizer has rational matrices. A nonzero fixed vector of the orbit group would therefore supply a nonzero rational fixed vector. The finite-orbit recurrence argument annihilates one coordinate of its image in the lattice's rational row space, contradicting genericity. This is the fixed-space obstruction used to exclude singleton root blocks.

  1. lemma OAI.DukePrimeDegree.vecMul_slMatrixConjugation_fixed_iff line 24
  2. lemma OAI.DukePrimeDegree.rational_fixedVector_fixes_pointOrbitStabilizer line 41
  3. lemma OAI.DukePrimeDegree.exists_rational_fixedVector_of_fixedVector line 58
  4. theorem OAI.DukePrimeDegree.fixedVector_eq_zero_of_generic_finite_root_orbit line 87

    Source documentation

    A finite-volume orbit through a generic lattice cannot simultaneously contain a nontrivial root group and fix a nonzero vector.

    theorem fixedVector_eq_zero_of_generic_finite_root_orbit {n : ℕ}
    (g : G n)
    (hgeneric : ∀ 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) = μ)
    (i j : Fin n) (hij : i ≠ j)
    (hroot : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ H)
    (v : Fin n → ℝ) (hv : ∀ h : H, v ᵥ* h.val.val = v) : v = 0 := by
…

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