The Bing-Borsuk Conjecture #
The Bing-Borsuk conjecture states that every $n$-dimensional homogeneous absolute neighborhood retract is a topological $n$-manifold.
The conjecture has been verified in dimensions $1$ and $2$ but remains open in higher dimensions. A notable consequence is that if the $3$-dimensional case is true, it implies the Poincaré conjecture.
References:
- Wikipedia
- [HR2008] Halverson, Denise M., and Dušan Repovš. "The Bing-Borsuk and the Busemann conjectures." Mathematical Communications 13.2 (2008): 163-184. https://arxiv.org/abs/0811.0886
theorem
BingBorsuk.bing_borsuk_conjecture
(n : ℕ)
(X : Type)
[TopologicalSpace X]
[TopologicalSpace.MetrizableSpace X]
[HomogeneousSpace X]
[IsAbsoluteNeighborhoodRetract X]
:
HasLebesgueCoveringDimensionEq X n → Nonempty (ChartedSpace (Fin n → ℝ) X)
The Bing-Borsuk Conjecture: every $n$-dimensional homogeneous absolute neighborhood retract
is a topological $n$-manifold. A topological space $X$ is an $n$-dimensional manifold
when T2Space X ∧ Nonempty (ChartedSpace (Fin n → ℝ) X). The hypothesis [MetrizableSpace X]
implies T2Space X so this does not appear in the conclusion.