/-
Copyright 2026 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 FormalConjecturesUtilHilbert'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.
References:
[van den Dries–Goldbring, Hilbert's Fifth Problem] (https://ems.press/journals/lem/articles/13621)
namespace Hilbert5open scoped Manifold ContDiff EuclideanGeometryuniverse uvariable {G : Type*} [Group G] [TopologicalSpace G]variable {n : ℕ} {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) X]
A continuous group isomorphism from G to an n-dimensional real-analytic Lie group.
structure LieGroupPresentation (G : Type u) [TopologicalSpace G] [Group G] (n : ℕ) where
carrier : Type u
[topologicalSpace : TopologicalSpace carrier]
[group : Group carrier]
[t2Space : T2Space carrier]
[secondCountableTopology : SecondCountableTopology carrier]
[chartedSpace : ChartedSpace (EuclideanSpace ℝ (Fin n)) carrier]
[isManifold : IsManifold (𝓡 n) ω carrier]
[lieGroup : LieGroup (𝓡 n) ω carrier]
equiv : G ≃ₜ* carrier
A topological group admits a Lie group structure if it has a LieGroupPresentation in some
finite dimension.
def AdmitsLieGroupStructure (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∃ n, Nonempty (LieGroupPresentation G n)Every finite-dimensional real-analytic Lie group admits a Lie group structure.
@[category API, AMS 22]
theorem admitsLieGroupStructure_of_lieGroup
[T2Space G] [SecondCountableTopology G]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) G]
[LieGroup (𝓡 n) ω G] :
AdmitsLieGroupStructure G :=
⟨n, ⟨{ carrier := G, equiv := ContinuousMulEquiv.refl G }⟩⟩A group admitting a Lie group structure is locally compact.
@[category API, AMS 22]
theorem locallyCompact_of_admitsLieGroupStructure
(h : AdmitsLieGroupStructure G) : LocallyCompactSpace G := G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gh:AdmitsLieGroupStructure G⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G k⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis:TopologicalSpace p.carrier := p.topologicalSpace⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝:TopologicalSpace p.carrier := p.topologicalSpacethis:Group p.carrier := p.group⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝¹:TopologicalSpace p.carrier := p.topologicalSpacethis✝:Group p.carrier := p.groupthis:ChartedSpace (ℝ^k) p.carrier := p.chartedSpace⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝²:TopologicalSpace p.carrier := p.topologicalSpacethis✝¹:Group p.carrier := p.groupthis✝:ChartedSpace (ℝ^k) p.carrier := p.chartedSpacethis:LocallyCompactSpace (ℝ^k)⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝³:TopologicalSpace p.carrier := p.topologicalSpacethis✝²:Group p.carrier := p.groupthis✝¹:ChartedSpace (ℝ^k) p.carrier := p.chartedSpacethis✝:LocallyCompactSpace (ℝ^k)this:LocallyCompactSpace p.carrier⊢ LocallyCompactSpace G
All goals completed! 🐙Hilbert–Smith conjecture: every locally compact topological group acting continuously and faithfully on a connected finite-dimensional topological manifold is a Lie group.
@[category research open, AMS 22 57 58]
theorem hilbert_smith_conjecture
[IsTopologicalGroup G] [LocallyCompactSpace G]
[MulAction G X] [ContinuousSMul G X] [FaithfulSMul G X] :
AdmitsLieGroupStructure G := G:Type u_1inst✝⁹:Group Ginst✝⁸:TopologicalSpace GX:Type u_2inst✝⁷:TopologicalSpace Xinst✝⁶:T2Space Xinst✝⁵:ConnectedSpace Xinst✝⁴:IsTopologicalGroup Ginst✝³:LocallyCompactSpace Ginst✝²:MulAction G Xinst✝¹:ContinuousSMul G Xinst✝:FaithfulSMul G X⊢ AdmitsLieGroupStructure G
All goals completed! 🐙
The conjecture holds when G acts by isometries on a Riemannian manifold, since G
embeds as a closed subgroup of the isometry group, which is a Lie group by Myers–Steenrod.
@[category research solved, AMS 22 53 57 58]
theorem hilbert_smith_conjecture.variants.riemannian
[IsTopologicalGroup G] [LocallyCompactSpace G]
[MulAction G X] [ContinuousSMul G X] [FaithfulSMul G X]
[MetricSpace X] [IsManifold (𝓡 n) ∞ X]
(hiso : ∀ g : G, Isometry (g • · : X → X)) :
AdmitsLieGroupStructure G := G:Type u_1inst✝¹²:Group Ginst✝¹¹:TopologicalSpace Gn:ℕX:Type u_2inst✝¹⁰:TopologicalSpace Xinst✝⁹:T2Space Xinst✝⁸:ConnectedSpace Xinst✝⁷:ChartedSpace (ℝ^n) Xinst✝⁶:IsTopologicalGroup Ginst✝⁵:LocallyCompactSpace Ginst✝⁴:MulAction G Xinst✝³:ContinuousSMul G Xinst✝²:FaithfulSMul G Xinst✝¹:MetricSpace Xinst✝:IsManifold (𝓡 n) ∞ Xhiso:∀ (g : G), Isometry fun x ↦ g • x⊢ AdmitsLieGroupStructure G
All goals completed! 🐙Pardon (2013): the Hilbert–Smith conjecture holds for 3-dimensional manifolds. See arXiv:1112.2324.
@[category research solved, AMS 22 57 58]
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 := G:Type u_1inst✝¹⁰:Group Ginst✝⁹:TopologicalSpace GX:Type u_3inst✝⁸:TopologicalSpace Xinst✝⁷:T2Space Xinst✝⁶:ConnectedSpace Xinst✝⁵:ChartedSpace ℝ³ Xinst✝⁴:IsTopologicalGroup Ginst✝³:LocallyCompactSpace Ginst✝²:MulAction G Xinst✝¹:ContinuousSMul G Xinst✝:FaithfulSMul G X⊢ AdmitsLieGroupStructure G
All goals completed! 🐙
Equivalent p-adic formulation: the p-adic integers ℤ_[p] cannot act continuously and
faithfully on any connected finite-dimensional topological manifold. By the Gleason–Yamabe
theorem, this is equivalent to hilbert_smith_conjecture.
@[category research open, AMS 22 57 58]
theorem hilbert_smith_padic_formulation (p : ℕ) [Fact p.Prime]
[AddAction (PadicInt p) X] [ContinuousVAdd (PadicInt p) X]
[FaithfulVAdd (PadicInt p) X] :
False := X:Type u_2inst✝⁶:TopologicalSpace Xinst✝⁵:T2Space Xinst✝⁴:ConnectedSpace Xp:ℕinst✝³:Fact (Nat.Prime p)inst✝²:AddAction ℤ_[p] Xinst✝¹:ContinuousVAdd ℤ_[p] Xinst✝:FaithfulVAdd ℤ_[p] X⊢ False
All goals completed! 🐙Hilbert's fifth problem (Gleason–Montgomery–Zippin, 1952): every Hausdorff, second-countable 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.
@[category research solved, AMS 22 57]
theorem hilbert_fifth_problem
[IsTopologicalGroup G] [T2Space G] [SecondCountableTopology G]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) G] :
Nonempty (LieGroupPresentation G n) := G:Type u_1inst✝⁵:Group Ginst✝⁴:TopologicalSpace Gn:ℕinst✝³:IsTopologicalGroup Ginst✝²:T2Space Ginst✝¹:SecondCountableTopology Ginst✝:ChartedSpace (ℝ^n) G⊢ Nonempty (LieGroupPresentation G n)
All goals completed! 🐙end Hilbert5