The Annulus Theorem in dimension ≥ 5 (Kirby)

annulus_theorem_high_dim

Submitter: Kim Morrison.

Notes: The closed region between two disjoint, nested, locally flat embedded (n-1)-spheres in ℝⁿ (n ≥ 5) is homeomorphic to Sⁿ⁻¹ × [0,1]. Local flatness is essential (the Alexander horned sphere is a counterexample without it). This was the hard core of Kirby's stable-homeomorphism work, via the torus trick. The 'inside' of a sphere is defined via bounded complementary components rather than the Jordan–Brouwer theorem, which Mathlib lacks; for locally flat nested spheres the inside of g is automatically inside f, so it is not assumed. Paired with annulus_theorem_dim_four, the much harder n = 4 case (Quinn).

Source: R. C. Kirby, *Stable homeomorphisms and the annulus conjecture*, Ann. of Math. 89 (1969).

Informal solution: No formalization is feasible today: there is no Jordan–Brouwer separation, no theory of locally flat embeddings, and none of Kirby's torus-trick / stable-homeomorphism machinery in Mathlib.

theorem declaration uses `sorry`annulus_theorem_high_dim {n : ℕ} [NeZero n] (hn : 5 ≤ n)
    (f g : LeanEval.Topology.FlatSphere n)
    (hdisj : Disjoint (Set.range f.toFun) (Set.range g.toFun))
    (hnest : Set.range g.toFun ⊆ LeanEval.Topology.inside (Set.range f.toFun)) :
    Nonempty ((LeanEval.Topology.regionBetween f g) ≃ₜ (LeanEval.Topology.Sph n × I)) := byn:ℕinst✝:NeZero nhn:5 ≤ nf:FlatSphere ng:FlatSphere nhdisj:Disjoint (Set.range f.toFun) (Set.range g.toFun)hnest:Set.range g.toFun ⊆ inside (Set.range f.toFun)⊢ Nonempty (↑(LeanEval.Topology.regionBetween f g) ≃ₜ ↑(Sph n) × ↑I)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.