Surgery on a framed sphere #
Let E and F be normed groups, with unit spheres S = sphere 0 1 and closed unit balls
D = closedBall 0 1. For E = ℝᵏ⁺¹ and F = ℝ^q these are Sᵏ ⊆ Dᵏ⁺¹ and S^(q-1) ⊆ D^q.
Throughout, int D and ∂D name the norm-level subsets ‖y‖ < 1 and ‖y‖ = 1 of D, and the
boundary of a product of balls and spheres is the subset where the ball coordinate has norm 1.
These are definitions, not topological statements: when E is a real normed space, int D and
∂D are the topological interior and frontier of D in E (interior_closedBall,
frontier_closedBall), and for E = ℝᵏ⁺¹ they are the manifold interior and boundary of Dᵏ⁺¹. A
framed sphere in a space M is a map φ : Sᵏ × D^q → M, typically an embedding: an embedded
k-sphere together with a trivialization of a closed tubular neighbourhood. Surgery along φ
removes the open tube φ (Sᵏ × int D^q) from M and glues in D^(k+1) × S^(q-1) along the
common boundary Sᵏ × S^(q-1), the point (x, y) of ∂D^(k+1) × S^(q-1) being glued to
φ (x, y). For k = 1 and q = 2 this is integral Dehn surgery on a framed knot in a
3-manifold, and for k = 0 it removes two balls and joins their boundary spheres by a tube
D¹ × S^(q-1).
Here a surgery is recorded inside the resulting space, without a gluing construction, in the same
way as TauCeti.DehnFilling and TauCeti.HeegaardSplitting: a TauCeti.SphereSurgery hφ Y
consists of closed embeddings into Y of the exterior TauCeti.sphereExterior φ of the framed
sphere and of D^(k+1) × S^(q-1), whose images cover Y and meet only along the boundary of
D^(k+1) × S^(q-1), where they are identified as above. The two pieces being closed, a continuous
map on Y is the same as a pair of continuous maps on the pieces agreeing on the boundary
(TauCeti.SphereSurgery.desc, TauCeti.SphereSurgery.desc_unique), so Y is homeomorphic to the
space obtained by gluing.
Main definitions #
TauCeti.sphereExterior φ: the complement inMof the open tubeφ (Sᵏ × int D^q).TauCeti.sphereExteriorBoundaryInclusion hφ: the boundarySᵏ × S^(q-1)of the exterior, parametrized throughφ.TauCeti.ballSphereBoundaryInclusion: the inclusion ofSᵏ × S^(q-1)intoD^(k+1) × S^(q-1).TauCeti.SphereSurgery hφ Y: a surgery along the framed sphereφ, recorded insideY.TauCeti.SphereSurgery.desc: the continuous map on the result of a surgery glued from compatible continuous maps on the two pieces.TauCeti.SphereSurgery.transHomeomorph: transport of a surgery along a homeomorphism.
Main results #
TauCeti.SphereSurgery.range_inter_range: the two pieces meet exactly in the boundary ofD^(k+1) × S^(q-1).TauCeti.SphereSurgery.hom_extandTauCeti.SphereSurgery.desc_unique: a continuous map on the result of a surgery is determined by its restrictions to the two pieces.
References #
- J. Milnor, A procedure for killing homotopy groups of differentiable manifolds, Proc. Sympos. Pure Math. 3 (1961), 39–55, Section 1 (spherical modifications).
- A. Ranicki, Algebraic and Geometric Surgery, Oxford Mathematical Monographs (2002), Chapter 1 (surgery on a framed embedded sphere).
The exterior of a framed sphere #
The inclusion of Sᵏ × S^(q-1) as the boundary Sᵏ × ∂D^q of the tube Sᵏ × D^q, the points
whose disc coordinate has norm 1.
Instances For
The boundary inclusion into the tube is continuous.
The sphere coordinate of a boundary point of the tube.
The disc coordinate of a boundary point of the tube lies on ∂D^q.
The inclusion of Sᵏ × S^(q-1) as the boundary ∂D^(k+1) × S^(q-1) of
D^(k+1) × S^(q-1), the points whose disc coordinate has norm 1.
Instances For
The boundary inclusion into the replacement piece is continuous.
The disc coordinate of a boundary point of D^(k+1) × S^(q-1) lies on ∂D^(k+1).
The sphere coordinate of a boundary point of D^(k+1) × S^(q-1).
The boundary of D^(k+1) × S^(q-1) is the set of points (x, y) with ‖x‖ = 1.
The exterior of a framed sphere φ : Sᵏ × D^q → M: the complement of the image of the open
tube Sᵏ × int D^q, the points whose disc coordinate has norm less than 1.
Instances For
A point lies in the exterior of a framed sphere when it is outside the open tube.
The boundary φ (Sᵏ × ∂D^q) of the tube of an injective framed sphere lies in its
exterior.
The boundary φ (Sᵏ × ∂D^q) of the exterior of an injective framed sphere, parametrized by
Sᵏ × S^(q-1) through the framing: q ↦ φ (q.1, q.2).
Instances For
The parametrized boundary of the exterior is q ↦ φ (q.1, q.2).
Surgery #
The parametrized boundary inclusion into the exterior is continuous when the framing is.
A surgery along the injective framed sphere φ : Sᵏ × D^q → M, recorded inside the
result Y: closed embeddings into Y of the exterior of φ and of D^(k+1) × S^(q-1), whose
images cover Y and meet only along the boundary of D^(k+1) × S^(q-1), the point (x, y) of
that boundary being the point φ (x, y) of the boundary of the exterior. The two images being
closed, Y is homeomorphic to the space obtained by gluing D^(k+1) × S^(q-1) to the exterior
along Sᵏ × S^(q-1).
- exteriorEmbedding : ↑(sphereExterior φ) → Y
The embedding of the exterior of the framed sphere into the result.
- isClosedEmbedding_exteriorEmbedding : Topology.IsClosedEmbedding self.exteriorEmbedding
- ballSphereEmbedding : ↑(Metric.closedBall 0 1) × ↑(Metric.sphere 0 1) → Y
The embedding of
D^(k+1) × S^(q-1)into the result. - isClosedEmbedding_ballSphereEmbedding : Topology.IsClosedEmbedding self.ballSphereEmbedding
- exteriorEmbedding_sphereExteriorBoundaryInclusion (q : ↑(Metric.sphere 0 1) × ↑(Metric.sphere 0 1)) : self.exteriorEmbedding (sphereExteriorBoundaryInclusion hφ q) = self.ballSphereEmbedding (ballSphereBoundaryInclusion q)
- range_union_range : Set.range self.exteriorEmbedding ∪ Set.range self.ballSphereEmbedding = Set.univ
- range_inter_range_subset : Set.range self.exteriorEmbedding ∩ Set.range self.ballSphereEmbedding ⊆ Set.range (self.ballSphereEmbedding ∘ ballSphereBoundaryInclusion)
Instances For
The two pieces of a surgery meet in the boundary of D^(k+1) × S^(q-1), which is the
image of the boundary of the exterior.
A point of the exterior is sent into D^(k+1) × S^(q-1) only on the boundary, where the two
are identified through the framing.
Maps out of the result of a surgery. Continuous maps a on the exterior and b on
D^(k+1) × S^(q-1) that agree along the boundary descend to a continuous map on the result,
which is the gluing of its two closed pieces (TauCeti.SphereSurgery.desc_unique).
Instances For
The map descended from a and b restricts to a on the exterior.
The map descended from a and b restricts to b on D^(k+1) × S^(q-1).
Maps out of the result of a surgery are determined by their restrictions to the two pieces.
Uniqueness of the descended map: a continuous map on the result of a surgery restricting
to a on the exterior and to b on D^(k+1) × S^(q-1) is TauCeti.SphereSurgery.desc.
A surgery is carried along a homeomorphism of its result.
Instances For
The exterior embedding of a transported surgery is the composite with the homeomorphism.
The embedding of D^(k+1) × S^(q-1) of a transported surgery is the composite with the
homeomorphism.