Hilbert's problems

The 2 problem files in FormalConjectures/HilbertProblems that state a research or textbook statement, at commit 2055e5ad, one article each.

Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.

TheoremHilbert's Fifth Problem and the Hilbert–Smith Conjecture#

The Hilbert–Smith conjecture states that a locally compact topological group acting continuously and faithfully on a connected finite-dimensional topological manifold must be a Lie group. It remains open in general; Pardon proved it for 3-manifolds in 2013. An equivalent formulation: no p-adic integer group ℤ_[p] can act faithfully on any connected finite-dimensional topological manifold.

Main statements

• hilbert_smith_conjecture: the Hilbert–Smith conjecture.
• hilbert_smith_padic_formulation: the equivalent formulation for ℤ_[p].
• hilbert_smith_conjecture.variants.dimension_three: Pardon's theorem for 3-manifolds.
• hilbert_smith_conjecture.variants.riemannian: the case of isometric actions on Riemannian manifolds.
• hilbert_fifth_problem: Hilbert's fifth problem, solved by Gleason, Montgomery and Zippin.

Implementation notes

AdmitsLieGroupStructure G, defined in FormalConjecturesForMathlib.Geometry.Manifold.LieGroupPresentation, says that G is continuously isomorphic to a finite-dimensional real-analytic Lie group. Lie groups are Hausdorff but not assumed second countable: every discrete group is a 0-dimensional Lie group (admitsLieGroupStructure_of_discreteTopology). This matters for the Hilbert–Smith conjecture, since uncountable discrete groups act continuously and faithfully on connected manifolds, for instance ℝ with the discrete topology acting on ℝ by translations.

The acting group is not assumed Hausdorff: a topological group acting continuously and faithfully on a Hausdorff space is Hausdorff, because the closure of the identity acts trivially.

The hypotheses on the manifold X are written in each theorem. A section variable [ChartedSpace (EuclideanSpace ℝ (Fin n)) X] is included only in a theorem that mentions n, so it would be dropped silently from a statement that mentions only X.

References: - Wikipedia - Tao's blog - [Pardon 2013] J. Pardon, The Hilbert–Smith conjecture for three-manifolds, J. Amer. Math. Soc. 26 (2013), 879–899. https://doi.org/10.1090/S0894-0347-2013-00766-3, arXiv:1112.2324 - [Myers–Steenrod 1939] S. B. Myers, N. E. Steenrod, The group of isometries of a Riemannian manifold, Ann. of Math. 40 (1939), 400–416. https://doi.org/10.2307/1968928 - [van den Dries–Goldbring 2015] L. van den Dries, I. Goldbring, Hilbert's 5th problem, Enseign. Math. 61 (2015), 3–43. https://doi.org/10.4171/LEM/61-1/2-2

Quoted from FormalConjectures/HilbertProblems/5.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 5 research or textbook statements: 2 open and 3 solved. It also has 2 test statements, counted here but not shown.

Hilbert5.hilbert_smith_conjecture

Open: stated without proof.

Hilbert–Smith conjecture: every locally compact topological group acting continuously and faithfully on a connected finite-dimensional topological manifold is a Lie group.

theorem hilbert_smith_conjecture {X : Type*}
    [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) X]
    [IsTopologicalGroup G] [LocallyCompactSpace G]
    [MulAction G X] [ContinuousSMul G X] [FaithfulSMul G X] :
    AdmitsLieGroupStructure G

Category research open; AMS 22 Topological groups, Lie groups, 57 Manifolds and cell complexes, 58 Global analysis, analysis on manifolds. Declared in FormalConjectures/HilbertProblems/5.lean, line 89.

Hilbert5.hilbert_smith_conjecture.variants.riemannian

Solved: stated here without proof.

The Hilbert–Smith conjecture holds for actions by isometries of a connected smooth Riemannian manifold X: the isometry group of X is a Lie group by the Myers–Steenrod theorem, so G has no small subgroups and is a Lie group by the Gleason–Montgomery–Zippin theorem.

Here X carries its Riemannian distance (IsRiemannianManifold), so the metric topology of X is its manifold topology.

theorem hilbert_smith_conjecture.variants.riemannian {X : Type*} [EMetricSpace X]
    [ConnectedSpace X] [ChartedSpace (EuclideanSpace ℝ (Fin n)) X] [IsManifold (𝓡 n) ∞ X]
    [Bundle.RiemannianBundle (fun x : X ↦ TangentSpace (𝓡 n) x)]
    [IsContMDiffRiemannianBundle (𝓡 n) ∞ (EuclideanSpace ℝ (Fin n))
      (fun x : X ↦ TangentSpace (𝓡 n) x)]
    [IsRiemannianManifold (𝓡 n) X]
    [IsTopologicalGroup G] [LocallyCompactSpace G]
    [MulAction G X] [ContinuousSMul G X] [FaithfulSMul G X]
    (hiso : ∀ g : G, Isometry (g • · : X → X)) :
    AdmitsLieGroupStructure G

Category research solved; AMS 22 Topological groups, Lie groups, 53 Differential geometry, 57 Manifolds and cell complexes, 58 Global analysis, analysis on manifolds. Declared in FormalConjectures/HilbertProblems/5.lean, line 104.

Hilbert5.hilbert_smith_conjecture.variants.dimension_three

Solved: stated here without proof.

Pardon's theorem (2013): the Hilbert–Smith conjecture holds for connected 3-manifolds, see [Pardon 2013].

theorem hilbert_smith_conjecture.variants.dimension_three {X : Type*}
    [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) X]
    [IsTopologicalGroup G] [LocallyCompactSpace G]
    [MulAction G X] [ContinuousSMul G X] [FaithfulSMul G X] :
    AdmitsLieGroupStructure G

Category research solved; AMS 22 Topological groups, Lie groups, 57 Manifolds and cell complexes, 58 Global analysis, analysis on manifolds. Declared in FormalConjectures/HilbertProblems/5.lean, line 119.

Hilbert5.hilbert_smith_padic_formulation

Open: stated without proof.

p-adic formulation: the p-adic integers ℤ_[p] cannot act continuously and faithfully on a connected finite-dimensional topological manifold. This is equivalent to hilbert_smith_conjecture by the Gleason–Yamabe theorem together with Newman's theorem on periodic transformations of manifolds.

theorem hilbert_smith_padic_formulation {X : Type*}
    [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) X]
    (p : ℕ) [Fact p.Prime] [AddAction ℤ_[p] X] [ContinuousVAdd ℤ_[p] X] :
    ¬ FaithfulVAdd ℤ_[p] X

Category research open; AMS 22 Topological groups, Lie groups, 57 Manifolds and cell complexes, 58 Global analysis, analysis on manifolds. Declared in FormalConjectures/HilbertProblems/5.lean, line 132.

Hilbert5.hilbert_fifth_problem

Solved: stated here without proof.

Hilbert's fifth problem (Gleason–Montgomery–Zippin, 1952): every Hausdorff topological group modeled on a finite-dimensional Euclidean space is continuously isomorphic to a real-analytic Lie group.

The input ChartedSpace supplies only a topological atlas. The compatible analytic atlas and analytic group operations belong to the output LieGroupPresentation.

theorem hilbert_fifth_problem
    [IsTopologicalGroup G] [T2Space G]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) G] :
    Nonempty (LieGroupPresentation G n)

Category research solved; AMS 22 Topological groups, Lie groups, 57 Manifolds and cell complexes. Declared in FormalConjectures/HilbertProblems/5.lean, line 146.

Sources

• FormalConjectures/HilbertProblems/5.lean at 2055e5ad
• Wikipedia

LeanHilbert5.hilbert_smith_conjecture · Hilbert5.hilbert_smith_conjecture.variants.riemannian · Hilbert5.hilbert_smith_conjecture.variants.dimension_three · Hilbert5.hilbert_smith_padic_formulation · Hilbert5.hilbert_fifth_problem

TheoremHilbert's 17th problem#

Let \(f(x_1, \dots, x_n)\) be a multivariable polynomial with real coefficients that takes only nonnegative values for all real inputs. Hilbert's 17th problem asks whether there exist rational functions \(g_1, \dots, g_m\) such that \(f = g_1^2 + g_2^2 + \cdots + g_m^2\). Resolved affirmatively by Artin in 1927. References: - Wikipedia - Motzkin, "The arithmetic-geometric inequality". In Shisha, Oved (ed.). Inequalities. Academic Press. pp. 205–224.

Quoted from FormalConjectures/HilbertProblems/17.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 2 solved and 2 textbook results. It also has 2 test statements, counted here but not shown.

Hilbert17.hilbert_17th_problem

Solved: stated here without proof.

Hilbert's 17th problem: every non-negative multivariate polynomial is a sum of squares of rational functions.

theorem hilbert_17th_problem {n : ℕ} (hn : 0 < n) (f : MvPolynomial (Fin n) ℝ)
    (h : ∀ x : Fin n → ℝ, 0 ≤ f.eval x) :
    ∃ (m : ℕ) (g : Fin m → MvRatFunc (Fin n) ℝ), algebraMap _ _ f = ∑ i, (g i) ^ 2

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/HilbertProblems/17.lean, line 43.

Hilbert17.f_nonneg

Textbook result, proved here.

The Motzkin polynomial is non-negative everywhere.

theorem f_nonneg : ∀ x y : ℝ, 0 ≤ f.eval ![x, y]

Category textbook; AMS 12 Field theory and polynomials. Declared in FormalConjectures/HilbertProblems/17.lean, line 59.

Hilbert17.f_not_sum_of_squares

Textbook result, stated without proof.

The Motzkin polynomial cannot be written as a sum of squares of polynomials.

theorem f_not_sum_of_squares :
    ¬∃ (n : ℕ) (hn : 0 < n) (S : Fin n → MvPolynomial (Fin 2) ℝ), f = ∑ i, S i ^ 2

Category textbook; AMS 12 Field theory and polynomials. Declared in FormalConjectures/HilbertProblems/17.lean, line 73.

Hilbert17.hilbert_17th_problem_poly

Solved: stated here without proof.

Hilbert's 17th problem for homogeneous polynomials: characterization of dimensions and degrees where non-negative polynomials are sums of squares of polynomials.

theorem hilbert_17th_problem_poly {n d : ℕ} (hn : 0 < n) (hd : 0 < d) :
    Hilbert17thProblemHomogenousPoly n d ↔ n = 1 ∨ n = 2 ∨ d = 1 ∨ n = 3 ∧ d = 2

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/HilbertProblems/17.lean, line 115.

Sources

• FormalConjectures/HilbertProblems/17.lean at 2055e5ad
• Wikipedia

LeanHilbert17.hilbert_17th_problem · Hilbert17.f_nonneg · Hilbert17.f_not_sum_of_squares · Hilbert17.hilbert_17th_problem_poly

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.