Absorbing an isotopy of the boundary into a radial collar #

Let E be a real normed space, S ⊆ E its unit sphere and D its closed unit ball, and let Z be any topological space. An ambient isotopy Φ of the boundary S × Z of D × Z extends to a homeomorphism of D × Z which is the identity on the inner ball ‖x‖ ≤ 1 / 2 and is the final homeomorphism Φ₁ of the isotopy on the boundary. The radial coordinate ‖x‖ ∈ [1 / 2, 1] serves as the time of the isotopy: in polar coordinates x = r • u,

(r • u, z) ↦ (r • Φ_t (u, z).1, Φ_t (u, z).2) with t = 2 r - 1 clamped to [0, 1].

So the boundary homeomorphisms of D × Z that extend over D × Z are closed under composition with homeomorphisms isotopic to the identity. This is the step of the classical proof that a gluing along the boundary depends only on the isotopy class of the gluing map, in which the isotopy is absorbed into a collar of the boundary (Rolfsen, Knots and Links, Section 9F, for Dehn fillings, where D × Z = D² × S¹ is the filling solid torus; with Z = S^(q-1) it is the handle D^(k+1) × S^(q-1) of surgery on a framed sphere).

The homeomorphism is first built on all of E × Z, where it preserves the norm of the first coordinate, and then restricted to D × Z.

Main definitions #

TauCeti.AmbientIsotopy.radialHomeomorph: the homeomorphism of E × Z running the ambient isotopy Φ of S × Z along the radial coordinate.
TauCeti.AmbientIsotopy.closedBallProdHomeomorph: its restriction to D × Z.

Main results #

TauCeti.AmbientIsotopy.radialHomeomorph_smul: the formula in polar coordinates.
TauCeti.AmbientIsotopy.norm_fst_radialHomeomorph: the norm of the first coordinate is preserved.
TauCeti.AmbientIsotopy.radialHomeomorph_of_norm_le: the identity on ‖x‖ ≤ 1 / 2.
TauCeti.AmbientIsotopy.radialHomeomorph_smul_of_one_le: the final homeomorphism of Φ, rescaled, on ‖x‖ ≥ 1.
TauCeti.AmbientIsotopy.closedBallProdHomeomorph_inclusion: on the boundary S × Z, the restriction to D × Z is the final homeomorphism of Φ.

References #

D. Rolfsen, Knots and Links, Publish or Perish (1976), Section 9F (the result of a Dehn filling depends only on the isotopy class of the gluing).

source

noncomputable def TauCeti.AmbientIsotopy.radialHomeomorph {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) :

E × Z ≃ₜ E × Z

The radial extension of an ambient isotopy Φ of S × Z, S the unit sphere of E: the homeomorphism (r • u, z) ↦ (r • Φ_t (u, z).1, Φ_t (u, z).2) of E × Z, for u ∈ S and r > 0, where the time t = 2 r - 1 is clamped to [0, 1]. It fixes {0} × Z, is the identity on ‖x‖ ≤ 1 / 2 (radialHomeomorph_of_norm_le), preserves ‖x‖ (norm_fst_radialHomeomorph) and on ‖x‖ ≥ 1 is the final homeomorphism of Φ, rescaled (radialHomeomorph_smul_of_one_le).

Instances For

source

theorem TauCeti.AmbientIsotopy.radialHomeomorph_smul {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) (u : ↑(Metric.sphere 0 1)) {r : ℝ} (hr : 0 < r) (z : Z) :

Φ.radialHomeomorph (r • ↑u, z) = (r • ↑(Φ.toContinuousMap (Set.projIcc 0 1 ⋯ (2 * r - 1), u, z)).1, (Φ.toContinuousMap (Set.projIcc 0 1 ⋯ (2 * r - 1), u, z)).2)

The radial extension in polar coordinates x = r • u, u in the unit sphere and r > 0: the isotopy is run on the sphere of radius r at the time 2 r - 1, clamped to [0, 1].

source

theorem TauCeti.AmbientIsotopy.symm_radialHomeomorph {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) :

Φ.radialHomeomorph.symm = Φ.symm.radialHomeomorph

The inverse of the radial extension of Φ is the radial extension of the inverse isotopy.

source

@[simp]

theorem TauCeti.AmbientIsotopy.norm_fst_radialHomeomorph {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) (p : E × Z) :

‖(Φ.radialHomeomorph p).1‖ = ‖p.1‖

The radial extension preserves the norm of the first coordinate.

source

theorem TauCeti.AmbientIsotopy.radialHomeomorph_of_norm_le {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) {p : E × Z} (hp : ‖p.1‖ ≤ 1 / 2) :

Φ.radialHomeomorph p = p

The radial extension is the identity on the inner ball ‖x‖ ≤ 1 / 2.

source

theorem TauCeti.AmbientIsotopy.radialHomeomorph_smul_of_one_le {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) (u : ↑(Metric.sphere 0 1)) {r : ℝ} (hr : 1 ≤ r) (z : Z) :

Φ.radialHomeomorph (r • ↑u, z) = (r • ↑(Φ.final (u, z)).1, (Φ.final (u, z)).2)

Outside the open unit ball the radial extension is the final homeomorphism of Φ, rescaled: (r • u, z) ↦ (r • Φ₁ (u, z).1, Φ₁ (u, z).2) for r ≥ 1.

source

theorem TauCeti.AmbientIsotopy.radialHomeomorph_coe_sphere {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) (q : ↑(Metric.sphere 0 1) × Z) :

Φ.radialHomeomorph (↑q.1, q.2) = (↑(Φ.final q).1, (Φ.final q).2)

On the unit sphere the radial extension is the final homeomorphism of Φ.

source

noncomputable def TauCeti.AmbientIsotopy.closedBallProdHomeomorph {E : Type u_1} {Z : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace Z] (Φ : AmbientIsotopy (↑(Metric.sphere 0 1) × Z)) :

↑(Metric.closedBall 0 1) × Z ≃ₜ ↑(Metric.closedBall 0 1) × Z

The extension of an ambient isotopy of S × Z over D × Z, S and D the unit sphere and closed unit ball of E: the restriction of radialHomeomorph to D × Z. It is the identity on ‖x‖ ≤ 1 / 2 (closedBallProdHomeomorph_of_norm_le) and the final homeomorphism of Φ on the boundary S × Z (closedBallProdHomeomorph_inclusion).