A conjecture by Margulis on matrix groups

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

instance instTopologicalSpaceSpecialLinearGroupReal_formalConjectures (n : Type u_1) [DecidableEq n] [Fintype n] : TopologicalSpace (Matrix.SpecialLinearGroup n ℝ)

Equations

• instTopologicalSpaceSpecialLinearGroupReal_formalConjectures n = inferInstanceAs (TopologicalSpace { A : Matrix n n ℝ // A.det = 1 })

theorem conjecture_1_1 {n : ℕ} (hn : 3 ≤ n) (g : Matrix.SpecialLinearGroup (Fin n) ℝ ⧸ Subgroup.map (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ⊤) (hg : IsCompact (closure (MulAction.orbit (↥(Matrix.SpecialLinearGroup.diagonalSubgroup (Fin n) ℝ)) g))) : IsClosed (MulAction.orbit (↥(Matrix.SpecialLinearGroup.diagonalSubgroup (Fin n) ℝ)) g)