/-
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.
namespace Hilbert5
open scoped Manifold ContDiff EuclideanGeometry
variable {G : Type*} [Group G] [TopologicalSpace G]variable {n : ℕ} {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) X]
A topological group G admits a Lie group structure if there exists a finite-dimensional
smooth manifold structure on G making it a real Lie group.
def AdmitsLieGroupStructure (G : Type*) [Group G] [TopologicalSpace G] : Prop :=
∃ (k : ℕ) (cs : ChartedSpace (EuclideanSpace ℝ (Fin k)) G),
letI := cs
LieGroup (𝓡 k) ⊤ GEvery Lie group trivially admits a Lie group structure.
@[category API, AMS 22]
theorem admitsLieGroupStructure_of_lieGroup
[ChartedSpace (EuclideanSpace ℝ (Fin n)) G] [LieGroup (𝓡 n) ⊤ G] :
AdmitsLieGroupStructure G :=
⟨n, inferInstance, inferInstance⟩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:ℕcs:ChartedSpace (ℝ^k) Gh✝:LieGroup (𝓡 k) ω G⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕcs:ChartedSpace (ℝ^k) Gh✝:LieGroup (𝓡 k) ω Gthis:ChartedSpace (ℝ^k) G := cs⊢ LocallyCompactSpace G
G:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕcs:ChartedSpace (ℝ^k) Gh✝:LieGroup (𝓡 k) ω Gthis✝:ChartedSpace (ℝ^k) G := csthis:LocallyCompactSpace (ℝ^k) := ModelWithCorners.locallyCompactSpace (𝓡 k)⊢ 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 locally Euclidean topological group is a Lie group.
@[category research solved, AMS 22 57]
theorem hilbert_fifth_problem
[IsTopologicalGroup G]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) G] :
LieGroup (𝓡 n) ⊤ G := G:Type u_1inst✝³:Group Ginst✝²:TopologicalSpace Gn:ℕinst✝¹:IsTopologicalGroup Ginst✝:ChartedSpace (ℝ^n) G⊢ LieGroup (𝓡 n) ω G
All goals completed! 🐙
end Hilbert5