Tubular-neighborhood data

This file records the topological part of a tubular-neighborhood chart. Smooth normal-bundle theorems provide such data for smooth embeddings; the structure here keeps that existence theorem separate from the interface consumed by disc and sphere bundle constructions.

The interface follows the tubular-neighborhood theorem of J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 6.24, and the corresponding existence theorem of M. Hirsch, Differential Topology, Theorem 6.3.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 6.24.
• M. Hirsch, Differential Topology, Theorem 6.3.

structure TauCeti.IsTubularNeighborhood {B : Type u_1} {F : Type u_2} {N : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] [TopologicalSpace N] (f : B → N) (U : Set (Bundle.TotalSpace F E)) (toFun : ↑U → N) : Prop

The data supplied by a tubular-neighborhood theorem.

U is an open, fiberwise star-shaped neighborhood of the zero section in a family of fibers. A vector-bundle or smooth normal-bundle construction can instantiate this interface with its additional linear and differentiable structure. toFun identifies U with an open subset of the ambient space N, and agrees with the given core embedding f on the zero section. The star-shaped condition is stated with real scalars in [0, 1], which is the form used by the radial deformation of a tubular neighborhood.

• isOpen : IsOpen U

  The tubular domain is open in the total space.

• zero_mem (x : B) : Bundle.zeroSection F E x ∈ U

  Every point of the core has its zero vector in the tubular domain.

• fiberwise_starConvex (x : B) : StarConvex ℝ 0 {v : E x | { proj := x, snd := v } ∈ U}

  Each fiber slice of the domain is star-convex at the zero vector.

• isOpenEmbedding : Topology.IsOpenEmbedding toFun

  The tubular chart is an open embedding.

• isEmbedding_f : Topology.IsEmbedding f

  The core map is an embedding.

• map_zeroSection (x : B) : toFun ⟨Bundle.zeroSection F E x, ⋯⟩ = f x

  The tubular chart restricts to the core map on the zero section.

• continuous_radial : Continuous fun (p : ↑(Set.Icc 0 1) × ↑U) => { proj := (↑p.2).proj, snd := ↑p.1 • (↑p.2).snd }

  Radial contraction is continuous on the interval and tubular domain.

  This explicit field records the topological compatibility needed by the deformation arguments consuming tubular-neighborhood data.

theorem TauCeti.isTubularNeighborhood_zeroSection {B : Type u_1} {F : Type u_2} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] (hzero : Topology.IsEmbedding (Bundle.zeroSection F E)) (hradial : Continuous fun (p : ↑(Set.Icc 0 1) × Bundle.TotalSpace F E) => { proj := p.2.proj, snd := ↑p.1 • p.2.snd }) : IsTubularNeighborhood (Bundle.zeroSection F E) Set.univ fun (x : ↑Set.univ) => ↑x

The canonical zero-section model on the whole total space.

The continuity hypothesis records the vector-bundle topology needed by the radial contraction; hzero supplies the embedding of the zero section.

def TauCeti.IsTubularNeighborhood.radialContraction {B : Type u_1} {F : Type u_2} {N : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] [TopologicalSpace N] {f : B → N} {U : Set (Bundle.TotalSpace F E)} {toFun : ↑U → N} (T : IsTubularNeighborhood f U toFun) : ↑(Set.Icc 0 1) × ↑U → ↑U

The radial contraction of a tubular neighborhood, with its image kept in the tubular domain by fiberwise_starConvex.

@[simp]

theorem TauCeti.IsTubularNeighborhood.coe_radialContraction {B : Type u_1} {F : Type u_2} {N : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] [TopologicalSpace N] {f : B → N} {U : Set (Bundle.TotalSpace F E)} {toFun : ↑U → N} (T : IsTubularNeighborhood f U toFun) (p : ↑(Set.Icc 0 1) × ↑U) : ↑(T.radialContraction p) = { proj := (↑p.2).proj, snd := ↑p.1 • (↑p.2).snd }

The underlying total-space point of the radial contraction.

theorem TauCeti.IsTubularNeighborhood.continuous_radialContraction {B : Type u_1} {F : Type u_2} {N : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] [TopologicalSpace N] {f : B → N} {U : Set (Bundle.TotalSpace F E)} {toFun : ↑U → N} (T : IsTubularNeighborhood f U toFun) : Continuous T.radialContraction

The radial contraction supplied by tubular-neighborhood data is continuous.

@[simp]

theorem TauCeti.IsTubularNeighborhood.radialContraction_one {B : Type u_1} {F : Type u_2} {N : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] [TopologicalSpace N] {f : B → N} {U : Set (Bundle.TotalSpace F E)} {toFun : ↑U → N} (T : IsTubularNeighborhood f U toFun) (u : ↑U) : T.radialContraction (1, u) = u

At time one, radial contraction is the identity.

@[simp]

theorem TauCeti.IsTubularNeighborhood.radialContraction_zero {B : Type u_1} {F : Type u_2} {N : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommGroup (E x)] [(x : B) → Module ℝ (E x)] [TopologicalSpace N] {f : B → N} {U : Set (Bundle.TotalSpace F E)} {toFun : ↑U → N} (T : IsTubularNeighborhood f U toFun) (u : ↑U) : T.radialContraction (0, u) = ⟨Bundle.zeroSection F E (↑u).proj, ⋯⟩

At time zero, radial contraction lands on the zero section.