The side of a bicollared hypersurface is a manifold with boundary

Let M be a topological (n + 1)-manifold and f : N → M an n-manifold with a bicollar b : N × ℝ → M (TauCeti.IsBicollar). A side of the bicollar is a set C ⊆ M which meets the bicollar exactly in its half b (N × [0, ∞)), and which is open in M away from the image of f. Cutting M along the image of f and keeping C produces a topological manifold with boundary: this file equips C with charts in the Euclidean half-space EuclideanHalfSpace (n + 1) and shows that its manifold boundary is exactly the image of f.

The charts are of two kinds.

• At a point of the image of f, the chart reads the bicollar backwards: a point b (y, t) with t ≥ 0 goes to the chart coordinates of y in N together with the normal coordinate t, assembled into a point of the half-space by TauCeti.EuclideanHalfSpace.collarDiffeomorph. The image of f is sent to the boundary hyperplane.
• At any other point of C, the chart is a chart of M, followed by a fixed homeomorphism of ℝⁿ⁺¹ onto the open half-space {x | 0 < x 0} (exponentiating the zeroth coordinate). These points are therefore interior points.

This is how the manifolds with boundary of geometric topology arise from closed manifolds: the exterior of a knot is the side of the boundary torus of a solid torus neighbourhood, and the complement of an open ball, deleted for a connected sum, is a side of the boundary sphere.

Main definitions

• TauCeti.IsBicollar.sideChartedSpace: the charted-space structure on a side of a bicollar, modelled on EuclideanHalfSpace (n + 1). Every charted space is a C⁰ manifold, so this is a topological manifold with boundary.

Main results

• TauCeti.IsBicollar.boundary_sideChartedSpace: the manifold boundary of the side is the image of f.
• TauCeti.IsBicollar.interior_sideChartedSpace: its manifold interior is the rest of the side.

Implementation notes

The charted-space structure depends on the chosen bicollar: a set C may be a side of several bicollars, so sideChartedSpace is a definition rather than an instance.

References

• M. Brown, Locally flat imbeddings of topological manifolds, Annals of Mathematics 75 (1962), 331–341, for bicollared hypersurfaces.
• D. Rolfsen, Knots and Links, Publish or Perish (1976), Section 9F, for knot exteriors as manifolds with boundary.

@[instance_reducible]

noncomputable def TauCeti.IsBicollar.sideChartedSpace {n : ℕ} {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [ChartedSpace (EuclideanSpace ℝ (Fin (n + 1))) M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) N] {f : N → M} {b : N × ℝ → M} {C : Set M} (hb : IsBicollar f b) (hC : b ⁻¹' C = Set.univ ×ˢ Set.Ici 0) (hCo : IsOpen (C \ Set.range f)) : ChartedSpace (EuclideanHalfSpace (n + 1)) ↑C

A side C of a bicollar b of f : N → M — a set meeting the bicollar exactly in its nonnegative half and open away from the image of f — is charted on the Euclidean half-space EuclideanHalfSpace (n + 1). The image of f is its manifold boundary (TauCeti.IsBicollar.boundary_sideChartedSpace).

theorem TauCeti.IsBicollar.boundary_sideChartedSpace {n : ℕ} {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [ChartedSpace (EuclideanSpace ℝ (Fin (n + 1))) M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) N] {f : N → M} {b : N × ℝ → M} {C : Set M} (hb : IsBicollar f b) (hC : b ⁻¹' C = Set.univ ×ˢ Set.Ici 0) (hCo : IsOpen (C \ Set.range f)) : ModelWithCorners.boundary ↑C = Subtype.val ⁻¹' Set.range f

The manifold boundary of a side of a bicollar of f is the image of f.

theorem TauCeti.IsBicollar.interior_sideChartedSpace {n : ℕ} {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [ChartedSpace (EuclideanSpace ℝ (Fin (n + 1))) M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) N] {f : N → M} {b : N × ℝ → M} {C : Set M} (hb : IsBicollar f b) (hC : b ⁻¹' C = Set.univ ×ˢ Set.Ici 0) (hCo : IsOpen (C \ Set.range f)) : ModelWithCorners.interior ↑C = Subtype.val ⁻¹' (Set.range f)ᶜ

The manifold interior of a side of a bicollar of f is the part of the side off the image of f.