FormalConjectures/Arxiv/2504.17644/Margulis.lean

GitHub source file

3 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Margulis.conjecture_1_1 Let D be the diagonal group of SL_n(ℝ) where n ≥ 3 sorry line 42 source

   Source documentation

   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.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, HasQuotient.Quotient, Matrix.SpecialLinearGroup, Fin, Real, Subgroup, Subgroup.map, Int, Matrix.SpecialLinearGroup.map, Int.castRingHom, Top.top, IsCompact, closure, MulAction.orbit, Subtype, Membership.mem, Matrix.SpecialLinearGroup.diagonalSubgroup, IsClosed

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   50 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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 := by
   …

2. def Margulis.polyToLaurent The natural inclusion F[t] →+* F((t⁻¹)) line 75 source

   Source documentation

   The natural inclusion F[t] →+* F((t⁻¹)). The field F((t⁻¹)) is modelled by the Laurent series field F⸨X⸩, whose variable X plays the role of t⁻¹, so the polynomial variable t is sent to X⁻¹.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, RingHom, Polynomial, LaurentSeries, Int

   Proof uses: Polynomial.eval₂RingHom, HahnSeries.C, ZeroHom, HahnSeries, HahnSeries.single, Neg.neg, OfNat.ofNat

   49 instances, coercions and auxiliary constants left out.

   noncomputable def polyToLaurent : F[X] →+* F⸨X⸩ :=
   …

3. theorem Margulis.huang_shi_theorem_1_2 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] sorry line 97 source

   Source documentation

   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]. Here K is modelled by the Laurent series field F⸨X⸩ with X = t⁻¹, so that A is embedded via t ↦ X⁻¹. 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.

   depends on sorry what this means

   Statement uses: Field, Fintype, Membership.mem, Nat, Finset, Insert.insert, OfNat.ofNat, Singleton.singleton, ringChar, Exists, HasQuotient.Quotient, Matrix.SpecialLinearGroup, Fin, LaurentSeries, Int, Subgroup, MonoidHom.range, Polynomial, Matrix.SpecialLinearGroup.map, Margulis.polyToLaurent and 8 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   86 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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) := by
   …

   Mentions: Margulis.polyToLaurent