The Annulus Theorem in dimension 4 (Quinn)

annulus_theorem_dim_four

Submitter: Kim Morrison.

Notes: The closed region between two disjoint, nested, locally flat embedded 3-spheres in ℝ⁴ is homeomorphic to S³ × [0,1]. This is the four-dimensional annulus theorem, of an entirely different difficulty from the n ≥ 5 case: it was settled by Quinn (1982), building on Freedman's topology of 4-manifolds. Same infrastructure as annulus_theorem_high_dim; local flatness is essential, and 'inside' is defined via bounded complementary components rather than the (absent) Jordan–Brouwer theorem.

Source: F. Quinn, *Ends of maps III: dimensions 4 and 5*, J. Differential Geom. 17 (1982), building on M. H. Freedman, *The topology of four-dimensional manifolds*, J. Differential Geom. 17 (1982).

Informal solution: No formalization is feasible today: this needs Freedman–Quinn 4-dimensional topology (Casson handles, the disk embedding theorem), none of which is in Mathlib, on top of the missing Jordan–Brouwer separation and locally-flat-embedding theory.

theorem declaration uses `sorry`annulus_theorem_dim_four (f g : LeanEval.Topology.FlatSphere 4)
    (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 4 × I)) := byf:FlatSphere 4g:FlatSphere 4hdisj: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 4) × ↑I)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.