Knot exteriors from solid-torus neighbourhoods

The exterior of a framed knot is the complement of the open solid torus in a solid-torus neighbourhood. This file gives that complement a named carrier and records the compactness and boundary facts needed by Dehn filling.

It also makes the exterior a topological manifold with boundary when the ambient space is a Hausdorff topological 3-manifold. A solid torus neighbourhood Φ alone does not suffice for this, since nothing controls the ambient space just outside the image of Φ. Shrinking the solid torus to half its radius, Φ ∘ SolidTorus.halve, leaves room on both sides of the new boundary torus: the annuli {w | 0 < ‖w‖ < 1} of Φ give it a bicollar (TauCeti.IsSolidTorusNeighborhood.isBicollared_comp_halve_comp_boundaryInclusion), with the radius ‖w‖ = σ(t) read through the logistic sigmoid σ. The exterior of the shrunken neighbourhood is the outer side of this bicollar, so TauCeti.IsBicollar.sideChartedSpace charts it on the half-space EuclideanHalfSpace 3, with manifold boundary the torus (TauCeti.IsSolidTorusNeighborhood.boundary_exteriorChartedSpace). This file constructs the topological charted-space structure.

Main definitions

• TauCeti.knotExterior: the exterior of a solid torus neighbourhood.
• TauCeti.IsSolidTorusNeighborhood.exteriorBoundaryInclusion: the boundary torus of the exterior, parametrized by S¹ × S¹ through Φ.
• TauCeti.IsSolidTorusNeighborhood.openExterior: the exterior without its boundary torus, the open complement of the closed solid torus.
• TauCeti.SolidTorus.halve: the solid torus of half the radius inside the solid torus.
• TauCeti.halveBicollar: the bicollar of its boundary torus, swept out by the annuli of Φ.
• TauCeti.IsSolidTorusNeighborhood.exteriorChartedSpace: the exterior of the half-radius neighbourhood, charted on the Euclidean half-space.

Main results

• TauCeti.IsSolidTorusNeighborhood.comp_halve: the half-radius solid torus is again a solid torus neighbourhood of the knot.
• TauCeti.IsSolidTorusNeighborhood.isBicollar_halveBicollar and TauCeti.IsSolidTorusNeighborhood.isBicollared_comp_halve_comp_boundaryInclusion: its boundary torus is bicollared.
• TauCeti.IsSolidTorusNeighborhood.preimage_halveBicollar_knotExterior: the exterior of the half-radius solid torus is the outer side of that bicollar.
• TauCeti.IsSolidTorusNeighborhood.boundary_exteriorChartedSpace: the manifold boundary of the exterior is the boundary torus.

The definition and its elementary topological properties follow Rolfsen, Knots and Links, Sections 2E and 9F.

def TauCeti.knotExterior {X : Type u_1} {Φ : SolidTorus → X} : Set X

The closed exterior of a solid-torus neighbourhood: the complement of its open solid-torus image.

@[simp]

theorem TauCeti.mem_knotExterior {X : Type u_1} {Φ : SolidTorus → X} {x : X} : x ∈ knotExterior ↔ x ∉ Φ '' {p : SolidTorus | ‖↑p.1‖ < 1}

Membership in the exterior means that a point is outside the open solid-torus image.

theorem TauCeti.knotExterior_sdiff_range {X : Type u_1} (Φ : SolidTorus → X) : knotExterior \ Set.range (Φ ∘ SolidTorus.boundaryInclusion) = (Set.range Φ)ᶜ

The exterior of a solid torus neighbourhood, with its boundary torus removed, is the complement of the closed solid torus.

theorem TauCeti.IsSolidTorusNeighborhood.isClosed_exterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsClosed knotExterior

The exterior is closed in any ambient topological space.

theorem TauCeti.IsSolidTorusNeighborhood.isCompact_exterior {X : Type u_1} [TopologicalSpace X] [CompactSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsCompact knotExterior

In a compact ambient space, the knot exterior is compact.

theorem TauCeti.IsSolidTorusNeighborhood.exterior_frontier {X : Type u_1} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : frontier knotExterior = Set.range (Φ ∘ SolidTorus.boundaryInclusion)

The framed boundary torus is the frontier of the knot exterior.

theorem TauCeti.IsSolidTorusNeighborhood.apply_boundaryInclusion_mem_knotExterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (q : Circle × Circle) : Φ (SolidTorus.boundaryInclusion q) ∈ knotExterior

The boundary torus of a solid torus neighbourhood lies in the knot exterior.

def TauCeti.IsSolidTorusNeighborhood.exteriorBoundaryInclusion {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (q : Circle × Circle) : ↑knotExterior

The boundary torus of the knot exterior, parametrized by S¹ × S¹ through the solid torus neighbourhood: q ↦ Φ (q.1, q.2).

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.coe_exteriorBoundaryInclusion_apply {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (q : Circle × Circle) : ↑(h.exteriorBoundaryInclusion q) = Φ (SolidTorus.boundaryInclusion q)

The parametrized boundary torus of the exterior is q ↦ Φ (q.1, q.2).

theorem TauCeti.IsSolidTorusNeighborhood.exteriorBoundaryInclusion_injective {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : Function.Injective h.exteriorBoundaryInclusion

The parametrization of the boundary torus of the exterior is injective.

theorem TauCeti.IsSolidTorusNeighborhood.isEmbedding_exteriorBoundaryInclusion {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : Topology.IsEmbedding h.exteriorBoundaryInclusion

The parametrization of the boundary torus of the exterior is an embedding.

def TauCeti.IsSolidTorusNeighborhood.openExterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : TopologicalSpace.Opens X

The open exterior of a solid torus neighbourhood Φ in a Hausdorff space: the complement of the closed solid torus range Φ, which is the knot exterior with its boundary torus removed (TauCeti.knotExterior_sdiff_range). In a 3-manifold it is the manifold interior of the exterior.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.coe_openExterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : ↑h.openExterior = (Set.range Φ)ᶜ

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.mem_openExterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) {x : X} : x ∈ h.openExterior ↔ x ∉ Set.range Φ

theorem TauCeti.IsSolidTorusNeighborhood.openExterior_subset_knotExterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : ↑h.openExterior ⊆ knotExterior

The open exterior lies in the knot exterior.

The half-radius solid torus

noncomputable def TauCeti.SolidTorus.halve (p : SolidTorus) : SolidTorus

The solid torus of half the radius inside the solid torus: (w, z) ↦ (w / 2, z).

@[simp]

theorem TauCeti.SolidTorus.coe_halve_fst (p : SolidTorus) : ↑p.halve.1 = 2⁻¹ • ↑p.1

@[simp]

theorem TauCeti.SolidTorus.halve_snd (p : SolidTorus) : p.halve.2 = p.2

theorem TauCeti.SolidTorus.isEmbedding_halve : Topology.IsEmbedding halve

Halving the radius is an embedding of the solid torus into itself.

theorem TauCeti.SolidTorus.image_halve_setOf_norm_lt_one : halve '' {p : SolidTorus | ‖↑p.1‖ < 1} = {p : SolidTorus | ‖↑p.1‖ < 2⁻¹}

Halving the radius maps the open solid torus onto the open solid torus of radius 1 / 2.

theorem TauCeti.IsSolidTorusNeighborhood.isOpenEmbedding_comp {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} {Y : Type u_2} [TopologicalSpace Y] (h : IsSolidTorusNeighborhood f Φ) {g : Y → SolidTorus} (hg : Topology.IsOpenEmbedding g) (hgO : Set.range g ⊆ {p : SolidTorus | ‖↑p.1‖ < 1}) : Topology.IsOpenEmbedding (Φ ∘ g)

A solid torus neighbourhood restricts to an open embedding on every open subset of the open solid torus.

theorem TauCeti.IsSolidTorusNeighborhood.comp_halve {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsSolidTorusNeighborhood f (Φ ∘ SolidTorus.halve)

The solid torus of half the radius is again a solid torus neighbourhood of the knot.

noncomputable def TauCeti.halveBicollar {X : Type u_1} (Φ : SolidTorus → X) (q : (Circle × Circle) × ℝ) : X

The bicollar of the boundary torus of the half-radius solid torus inside a solid torus neighbourhood Φ: ((u, z), t) ↦ Φ (σ(t) u, z), where σ is the logistic sigmoid. It meets the exterior of the half-radius solid torus exactly in its nonnegative half (TauCeti.IsSolidTorusNeighborhood.preimage_halveBicollar_knotExterior).

theorem TauCeti.range_halveBicollar_subset {X : Type u_1} (Φ : SolidTorus → X) : Set.range (halveBicollar Φ) ⊆ Set.range Φ

The bicollar of the half-radius boundary torus stays inside the solid torus.

theorem TauCeti.IsSolidTorusNeighborhood.isBicollar_halveBicollar {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsBicollar (Φ ∘ SolidTorus.halve ∘ SolidTorus.boundaryInclusion) (halveBicollar Φ)

TauCeti.halveBicollar Φ is a bicollar of the boundary torus of the half-radius solid torus inside a solid torus neighbourhood Φ.

theorem TauCeti.IsSolidTorusNeighborhood.isBicollared_comp_halve_comp_boundaryInclusion {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsBicollared (Φ ∘ SolidTorus.halve ∘ SolidTorus.boundaryInclusion)

The boundary torus of the half-radius solid torus inside a solid torus neighbourhood is bicollared.

theorem TauCeti.IsSolidTorusNeighborhood.preimage_halveBicollar_knotExterior {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : halveBicollar Φ ⁻¹' knotExterior = Set.univ ×ˢ Set.Ici 0

The bicollar TauCeti.halveBicollar Φ meets the exterior of the half-radius solid torus exactly in its nonnegative half.

@[instance_reducible]

noncomputable def TauCeti.IsSolidTorusNeighborhood.exteriorChartedSpace {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) X] (h : IsSolidTorusNeighborhood f Φ) : ChartedSpace (EuclideanHalfSpace 3) ↑knotExterior

The exterior of the half-radius solid torus inside a solid torus neighbourhood, in a Hausdorff topological 3-manifold, as a topological manifold with boundary: it is the outer side of the bicollar of its boundary torus, charted by TauCeti.IsBicollar.sideChartedSpace. Its manifold boundary is the boundary torus (TauCeti.IsSolidTorusNeighborhood.boundary_exteriorChartedSpace).

theorem TauCeti.IsSolidTorusNeighborhood.boundary_exteriorChartedSpace {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) X] (h : IsSolidTorusNeighborhood f Φ) : ModelWithCorners.boundary ↑knotExterior = Subtype.val ⁻¹' Set.range (Φ ∘ SolidTorus.halve ∘ SolidTorus.boundaryInclusion)

The manifold boundary of the exterior of the half-radius solid torus is its boundary torus.

theorem TauCeti.IsSolidTorusNeighborhood.interior_exteriorChartedSpace {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) X] (h : IsSolidTorusNeighborhood f Φ) : ModelWithCorners.interior ↑knotExterior = Subtype.val ⁻¹' (Set.range (Φ ∘ SolidTorus.halve))ᶜ

The manifold interior of the exterior of the half-radius solid torus is the complement of the closed solid torus.