Annulus theorem

AbbreviationAmbient Euclidean space#✓fully proved

For a natural number \(n\), the ambient space is the real Euclidean space \(\mathbb{R}^n\) of dimension \(n\), with coordinates indexed by \(0, \dots, n-1\) and the Euclidean norm.

abbrev Amb (n : ℕ) : Type := EuclideanSpace ℝ (Fin n)

Used by 8

Used byAnnulus theorem in dimension four · Annulus theorem in dimensions at least five · Locally flat embedded sphere · Inside of a set · Locally flat maps of the sphere · Model hyperplane · Region between two flat spheres · Unit sphere in Euclidean space

AbbreviationUnit sphere in Euclidean space#✓fully proved

For a natural number \(n\), the unit sphere \(S^{n-1} \subseteq \mathbb{R}^n\) is the set of points of \(\mathbb{R}^n\) at Euclidean distance \(1\) from the origin.

abbrev Sph (n : ℕ) : Set (Amb n) := sphere (0 : Amb n) 1

Uses 1 · Used by 5

Statement usesAmbient Euclidean space

Used byAnnulus theorem in dimension four · Annulus theorem in dimensions at least five · Locally flat embedded sphere · Locally flat maps of the sphere · Region between two flat spheres

DefinitionModel hyperplane#✓fully proved

For \(n \ge 1\), the model hyperplane in \(\mathbb{R}^n\) is the set of points \(x = (x_0, \dots, x_{n-1})\) whose first coordinate \(x_0\) is \(0\). It is the local model for a locally flat embedded sphere.

def modelHyperplane (n : ℕ) [NeZero n] : Set (Amb n) := {x | x 0 = 0}

Uses 1 · Used by 1

Statement usesAmbient Euclidean space

Used byLocally flat maps of the sphere

DefinitionLocally flat maps of the sphere#✓fully proved

Let \(n \ge 1\), let \(S^{n-1} \subseteq \mathbb{R}^n\) be the unit sphere and let \(H = \{x \in \mathbb{R}^n : x_0 = 0\}\) be the model hyperplane. A map \(c : S^{n-1} \to \mathbb{R}^n\) is locally flat if for every point \(p \in S^{n-1}\) there are open sets \(U, V \subseteq \mathbb{R}^n\) with \(c(p) \in U\) and a homeomorphism \(h : U \to V\) such that \(h(U \cap c(S^{n-1})) = V \cap H\).

def LocallyFlat {n : ℕ} [NeZero n] (c : Sph n → Amb n) : Prop :=
  ∀ p : Sph n, ∃ h : OpenPartialHomeomorph (Amb n) (Amb n),
    c p ∈ h.source ∧
    h.toFun '' (h.source ∩ Set.range c) = h.target ∩ modelHyperplane n

Uses 3 · Used by 1

Statement usesAmbient Euclidean space · Unit sphere in Euclidean space · Model hyperplane

Used byLocally flat embedded sphere

StructureLocally flat embedded sphere#✓fully proved

For \(n \ge 1\), a locally flat embedded \((n-1)\)-sphere in \(\mathbb{R}^n\) is a map \(f : S^{n-1} \to \mathbb{R}^n\) from the unit sphere that is continuous, injective and locally flat.

structure FlatSphere (n : ℕ) [NeZero n] where
  /-- The embedding. -/
  toFun : Sph n → Amb n
  /-- It is continuous. -/
  continuous : Continuous toFun
  /-- It is injective. -/
  injective : Function.Injective toFun
  /-- It is locally flat. -/
  flat : LocallyFlat toFun

Uses 3 · Used by 3

Statement usesAmbient Euclidean space · Locally flat maps of the sphere · Unit sphere in Euclidean space

Used byAnnulus theorem in dimension four · Annulus theorem in dimensions at least five · Region between two flat spheres

DefinitionInside of a set#✓fully proved

For a set \(S \subseteq \mathbb{R}^n\), the inside of \(S\) is the set of points \(x \notin S\) whose connected component in the complement \(\mathbb{R}^n \setminus S\) is bounded.

For the image of a locally flat embedded sphere, this is the open ball it bounds.

def inside {n : ℕ} (S : Set (Amb n)) : Set (Amb n) :=
  {x | x ∉ S ∧ Bornology.IsBounded (connectedComponentIn Sᶜ x)}

Uses 1 · Used by 3

Statement usesAmbient Euclidean space

Used byAnnulus theorem in dimension four · Annulus theorem in dimensions at least five · Region between two flat spheres

DefinitionRegion between two flat spheres#✓fully proved

Let \(n \ge 1\) and let \(f\) and \(g\) be locally flat embedded \((n-1)\)-spheres in \(\mathbb{R}^n\). The region between \(f\) and \(g\) is the closure of the inside of the image of \(f\) with the inside of the image of \(g\) removed, where the inside of a set \(S\) is the set of points \(x \notin S\) whose connected component in \(\mathbb{R}^n \setminus S\) is bounded.

def regionBetween {n : ℕ} [NeZero n] (f g : FlatSphere n) : Set (Amb n) :=
  closure (inside (Set.range f.toFun)) \ inside (Set.range g.toFun)

Uses 4 · Used by 2

Statement usesAmbient Euclidean space · Locally flat embedded sphere · Unit sphere in Euclidean space · Inside of a set

Used byAnnulus theorem in dimension four · Annulus theorem in dimensions at least five

TheoremAnnulus theorem in dimension four#●ready to prove

Let \(f\) and \(g\) be locally flat embedded \(3\)-spheres in \(\mathbb{R}^4\), that is, continuous injective locally flat maps \(S^3 \to \mathbb{R}^4\) from the unit sphere. Suppose that the images of \(f\) and \(g\) are disjoint and that the image of \(g\) lies in the inside of the image of \(f\), the set of points off the image of \(f\) whose connected component in its complement is bounded. Then the region between \(f\) and \(g\), the closure of the inside of the image of \(f\) minus the inside of the image of \(g\), is homeomorphic to \(S^3 \times [0, 1]\).

public theorem_wanted annulus_theorem_dim_four
    (f g : FlatSphere 4)
    (hdisj : Disjoint (Set.range f.toFun) (Set.range g.toFun))
    (hnest : Set.range g.toFun ⊆ inside (Set.range f.toFun)) :
    Nonempty ((regionBetween f g) ≃ₜ (Sph 4 × I))

Sources

• 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). Problem annulus_theorem_dim_four of the lean-eval benchmark.

Uses 5

Statement usesAmbient Euclidean space · Locally flat embedded sphere · Unit sphere in Euclidean space · Inside of a set · Region between two flat spheres

TheoremAnnulus theorem in dimensions at least five#●ready to prove

Let \(n \ge 5\) and let \(f\) and \(g\) be locally flat embedded \((n-1)\)-spheres in \(\mathbb{R}^n\), that is, continuous injective locally flat maps \(S^{n-1} \to \mathbb{R}^n\) from the unit sphere. Suppose that the images of \(f\) and \(g\) are disjoint and that the image of \(g\) lies in the inside of the image of \(f\), the set of points off the image of \(f\) whose connected component in its complement is bounded. Then the region between \(f\) and \(g\), the closure of the inside of the image of \(f\) minus the inside of the image of \(g\), is homeomorphic to \(S^{n-1} \times [0, 1]\).

public theorem_wanted annulus_theorem_high_dim {n : ℕ} [NeZero n] (hn : 5 ≤ n)
    (f g : FlatSphere n)
    (hdisj : Disjoint (Set.range f.toFun) (Set.range g.toFun))
    (hnest : Set.range g.toFun ⊆ inside (Set.range f.toFun)) :
    Nonempty ((regionBetween f g) ≃ₜ (Sph n × I))

Sources

• R. C. Kirby, Stable homeomorphisms and the annulus conjecture, Ann. of Math. 89 (1969). Problem annulus_theorem_high_dim of the lean-eval benchmark.

Uses 5

Statement usesAmbient Euclidean space · Locally flat embedded sphere · Unit sphere in Euclidean space · Inside of a set · Region between two flat spheres

7 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.