1. FormalConjectures
  2. Arxiv
  3. «2504.17644»
  4. Margulis
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

A conjecture by Margulis on matrix groups

Reference: arxiv/2504.17644v3 Bounded diagonal orbits in homogeneous spaces over function fields by Qianlin Huang, Ronggang Shi

namespace Margulisopen Matrix SpecialLinearGroupopen scoped MatrixGroups Polynomial LaurentSeriessectionvariable (n : Type*) [DecidableEq n] [Fintype n] (R : Type*) [CommRing R]

Let D be the diagonal group of SL_n(ℝ) where n ≥ 3. Then any relatively compact D-orbit in SL_n(ℝ) / SL_n(ℤ) is closed.

@[category research open, AMS 11 15 22] theorem conjecture_1_1 {n : ℕ} (hn : 3 ≤ n) (g : SL(n, ℝ) ⧸ Subgroup.map (map (Int.castRingHom ℝ)) ⊤) (hg : IsCompact <| closure (MulAction.orbit (diagonalSubgroup (Fin n) ℝ) g)) : IsClosed <| MulAction.orbit (diagonalSubgroup (Fin n) ℝ) g := n:ℕhn:3 ≤ ng:SL(n, ℝ) ⧸ Subgroup.map (SpecialLinearGroup.map (Int.castRingHom ℝ)) ⊤hg:IsCompact (closure (MulAction.orbit (↥(diagonalSubgroup (Fin n) ℝ)) g))⊢ IsClosed (MulAction.orbit (↥(diagonalSubgroup (Fin n) ℝ)) g) All goals completed! 🐙end/- ## Diagonal orbits over function fields (Huang–Shi, Theorem 1.2) We now formulate a Lean version of the main theorem of Huang–Shi. Let `F` be a finite field of characteristic `p ∈ {3, 5, 7, 11}`. Set * `A = F[t]`, * `K = F((t⁻¹))`. Denote by `D` the diagonal subgroup of `SL₄(K)` and by `Γ` the lattice subgroup `SL₄(A)` embedded into `SL₄(K)` via the natural map `A →+* K`. Then there exists a point `z : SL₄(K)/Γ` such that the `D`-orbit of `z` has compact closure but is not closed. -/ universe usection FunctionFieldDiagonalOrbitvariable (F : Type u) [Field F] [Fintype F]

The natural inclusion F[t] →+* F((t⁻¹)).

noncomputable def polyToLaurent : F[X] →+* F⸨X⸩ := (HahnSeries.ofPowerSeries ℤ F).comp Polynomial.coeToPowerSeries.ringHom-- The `SetLike.GradeZero` instances for `Semiring`/`CommSemiring`/`Ring`/`CommRing`/`Monoid`/ -- `Algebra` on a grade-zero piece are stated for an arbitrary graded family and unify with -- `↥(diagonalSubgroup ...)` before being ruled out attribute [-instance] SetLike.GradeZero.instMonoid SetLike.GradeZero.instSemiring SetLike.GradeZero.instCommSemiring SetLike.GradeZero.instAlgebraSubtypeMemOfNat SetLike.GradeZero.instRing SetLike.GradeZero.instCommRing in

Huang–Shi, Theorem 1.2

Let F be a finite field of characteristic p ∈ {3, 5, 7, 11}, and set K = F((t⁻¹)), A = F[t]. Let

    D be the diagonal subgroup of SL₄(K),

    Γ = SL₄(A) the lattice subgroup embedded into SL₄(K) via the natural inclusion A →+* K.

Then there exists z : SL₄(K)/Γ such that the D-orbit of z has compact closure but is not closed.

@[category research solved, AMS 11 15 22] theorem huang_shi_theorem_1_2 (hchar : ringChar F ∈ ({3, 5, 7, 11} : Finset ℕ)) : ∃ z : SL(4, F⸨X⸩) ⧸ ( Matrix.SpecialLinearGroup.map (polyToLaurent F)).range, IsCompact (closure (MulAction.orbit (diagonalSubgroup (Fin 4) (F⸨X⸩)) z)) ∧ ¬ IsClosed (MulAction.orbit (diagonalSubgroup (Fin 4) (F⸨X⸩)) z) := F:Type uinst✝¹:Field Finst✝:Fintype Fhchar:ringChar F ∈ {3, 5, 7, 11}⊢ ∃ z, IsCompact (closure (MulAction.orbit (↥(diagonalSubgroup (Fin 4) F⸨X⸩)) z)) ∧ ¬IsClosed (MulAction.orbit (↥(diagonalSubgroup (Fin 4) F⸨X⸩)) z) -- Placeholder: a Lean formalization would require a full development -- of the Huang–Shi paper in mathlib. All goals completed! 🐙end FunctionFieldDiagonalOrbitend Margulis