Annulus coordinates on the Euclidean disk

For 0 < d ≤ 1, a point w of the annulus d ≤ ‖w‖ ≤ 1 of the disk TopCat.disk k is (d + (1 - d) s) • θ for a radial parameter s ∈ [0, 1] (TauCeti.TopCat.annulusParam) and a direction θ on the boundary sphere (TauCeti.TopCat.annulusDir). A map on the ball of radius d and a map on the annulus, given in these coordinates, glue to a map on the whole disk when they agree on the seam ‖w‖ = d (TauCeti.TopCat.discGlue). This is how a homotopy of a small disc is combined with a deformation of the surrounding annulus, as in cell reattachment arguments.

Main declarations

• TauCeti.TopCat.annulusParam, TauCeti.TopCat.annulusDir: the annulus coordinates.
• TauCeti.TopCat.add_one_sub_mul_annulusParam_smul_annulusDir: a point of the annulus is recovered from its coordinates.
• TauCeti.TopCat.discGlue: the gluing of a map on the ball of radius d and a map on the annulus, with a parameter space P.

noncomputable def TauCeti.TopCat.annulusParam {k : ℕ} (d : ℝ) (w : ↑(TopCat.disk k)) : ↑unitInterval

The radial parameter s ∈ [0, 1] of a point w = (d + (1 - d) s) • θ of the annulus d ≤ ‖w‖ ≤ 1 of the disk.

theorem TauCeti.TopCat.continuous_annulusParam {k : ℕ} {d : ℝ} : Continuous (annulusParam d)

noncomputable def TauCeti.TopCat.annulusDir {k : ℕ} {d : ℝ} (hd : 0 < d) (w : { w : ↑(TopCat.disk k) // d ≤ ‖↑w.down‖ }) : ↑(TopCat.diskBoundary k)

The direction w / ‖w‖ of a point w of the annulus d ≤ ‖w‖ of the disk, for 0 < d: the end of the radial push TauCeti.TopCat.diskRadialPush with radius d.

theorem TauCeti.TopCat.continuous_annulusDir {k : ℕ} {d : ℝ} (hd : 0 < d) : Continuous (annulusDir hd)

theorem TauCeti.TopCat.coe_annulusDir {k : ℕ} {d : ℝ} (hd : 0 < d) (w : { w : ↑(TopCat.disk k) // d ≤ ‖↑w.down‖ }) : ↑(annulusDir hd w).down = ‖↑(↑w).down‖⁻¹ • ↑(↑w).down

The direction of w is w / ‖w‖.

theorem TauCeti.TopCat.diskBoundaryInclusion_annulusDir {k : ℕ} {d : ℝ} (hd : 0 < d) (w : { w : ↑(TopCat.disk k) // d ≤ ‖↑w.down‖ }) : (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) (annulusDir hd w) = (diskRadialPush k ⋯) (1, ↑w)

Viewed in the disk, the direction of w is the end of the radial push with radius d.

@[simp]

theorem TauCeti.TopCat.annulusDir_diskBoundaryInclusion {k : ℕ} {d : ℝ} (hd : 0 < d) (s : ↑(TopCat.diskBoundary k)) (hs : d ≤ ‖↑((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s).down‖) : annulusDir hd ⟨(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s, hs⟩ = s

The direction of a point of the boundary sphere is the point itself.

theorem TauCeti.TopCat.add_one_sub_mul_annulusParam {k : ℕ} {d : ℝ} (hd₁ : d ≤ 1) {w : ↑(TopCat.disk k)} (hw : d ≤ ‖↑w.down‖) : d + (1 - d) * ↑(annulusParam d w) = ‖↑w.down‖

The radius d + (1 - d) s of the annulus coordinates of w is the norm of w.

theorem TauCeti.TopCat.add_one_sub_mul_annulusParam_smul_annulusDir {k : ℕ} {d : ℝ} (hd : 0 < d) (hd₁ : d ≤ 1) (w : { w : ↑(TopCat.disk k) // d ≤ ‖↑w.down‖ }) : (d + (1 - d) * ↑(annulusParam d ↑w)) • ↑(annulusDir hd w).down = ↑(↑w).down

A point of the annulus is recovered from its annulus coordinates.

theorem TauCeti.TopCat.annulusParam_of_norm_eq {k : ℕ} {d : ℝ} {w : ↑(TopCat.disk k)} (hw : ‖↑w.down‖ = d) : annulusParam d w = 0

On the seam ‖w‖ = d the radial parameter vanishes.

theorem TauCeti.TopCat.annulusParam_of_norm_le {k : ℕ} {d : ℝ} (hd₁ : d ≤ 1) {w : ↑(TopCat.disk k)} (hw : ‖↑w.down‖ ≤ d) : annulusParam d w = 0

Inside the ball of radius d the radial parameter vanishes, for d ≤ 1.

theorem TauCeti.TopCat.annulusParam_of_norm_eq_one {k : ℕ} {d : ℝ} (hd₁ : d < 1) {w : ↑(TopCat.disk k)} (hw : ‖↑w.down‖ = 1) : annulusParam d w = 1

On the boundary sphere the radial parameter is 1, for d < 1.

theorem TauCeti.TopCat.smul_diskBoundary_mem_closedBall {k : ℕ} {d : ℝ} (hd : 0 ≤ d) (θ : ↑(TopCat.diskBoundary k)) : d • ↑θ.down ∈ Metric.closedBall 0 d

The point d • θ of a point θ of the boundary sphere lies in the ball of radius d.

noncomputable def TauCeti.TopCat.discGlue {P : Type u_1} {Y : Type u_2} [TopologicalSpace P] [TopologicalSpace Y] {k : ℕ} {d : ℝ} (hd : 0 < d) (A : C(P × ↑(Metric.closedBall 0 d), Y)) (B : C(P × ↑unitInterval × ↑(TopCat.diskBoundary k), Y)) (hAB : ∀ (p : P) (θ : ↑(TopCat.diskBoundary k)), B (p, 0, θ) = A (p, ⟨d • ↑θ.down, ⋯⟩)) : C(P × ↑(TopCat.disk k), Y)

Glue a map on the ball of radius d of the disk to a map on the annulus d ≤ ‖w‖ ≤ 1, given in the coordinates (s, θ) of the point (d + (1 - d) s) • θ, when the two agree on the seam. Both maps may depend continuously on a parameter in P.

theorem TauCeti.TopCat.discGlue_apply_of_norm_le {P : Type u_1} {Y : Type u_2} [TopologicalSpace P] [TopologicalSpace Y] {k : ℕ} {d : ℝ} (hd : 0 < d) (A : C(P × ↑(Metric.closedBall 0 d), Y)) (B : C(P × ↑unitInterval × ↑(TopCat.diskBoundary k), Y)) (hAB : ∀ (p : P) (θ : ↑(TopCat.diskBoundary k)), B (p, 0, θ) = A (p, ⟨d • ↑θ.down, ⋯⟩)) (p : P) {w : ↑(TopCat.disk k)} (hw : ‖↑w.down‖ ≤ d) : (discGlue hd A B hAB) (p, w) = A (p, ⟨↑w.down, ⋯⟩)

On the ball of radius d a glued map is its inner piece.

theorem TauCeti.TopCat.discGlue_apply_of_le_norm {P : Type u_1} {Y : Type u_2} [TopologicalSpace P] [TopologicalSpace Y] {k : ℕ} {d : ℝ} (hd : 0 < d) (A : C(P × ↑(Metric.closedBall 0 d), Y)) (B : C(P × ↑unitInterval × ↑(TopCat.diskBoundary k), Y)) (hAB : ∀ (p : P) (θ : ↑(TopCat.diskBoundary k)), B (p, 0, θ) = A (p, ⟨d • ↑θ.down, ⋯⟩)) (p : P) {w : ↑(TopCat.disk k)} (hw : d ≤ ‖↑w.down‖) : (discGlue hd A B hAB) (p, w) = B (p, annulusParam d w, annulusDir hd ⟨w, hw⟩)

On the annulus d ≤ ‖w‖ a glued map is its outer piece, read in annulus coordinates.

theorem TauCeti.TopCat.discGlue_mem {P : Type u_1} {Y : Type u_2} [TopologicalSpace P] [TopologicalSpace Y] {k : ℕ} {d : ℝ} (hd : 0 < d) (A : C(P × ↑(Metric.closedBall 0 d), Y)) (B : C(P × ↑unitInterval × ↑(TopCat.diskBoundary k), Y)) (hAB : ∀ (p : P) (θ : ↑(TopCat.diskBoundary k)), B (p, 0, θ) = A (p, ⟨d • ↑θ.down, ⋯⟩)) {S : Set Y} (hA : ∀ (q : P × ↑(Metric.closedBall 0 d)), A q ∈ S) (hB : ∀ (q : P × ↑unitInterval × ↑(TopCat.diskBoundary k)), B q ∈ S) (q : P × ↑(TopCat.disk k)) : (discGlue hd A B hAB) q ∈ S

A glued map takes values in a set containing all values of both pieces.

theorem TauCeti.TopCat.discGlue_mem_of_norm_eq_one {P : Type u_1} {Y : Type u_2} [TopologicalSpace P] [TopologicalSpace Y] {k : ℕ} {d : ℝ} (hd : 0 < d) (A : C(P × ↑(Metric.closedBall 0 d), Y)) (B : C(P × ↑unitInterval × ↑(TopCat.diskBoundary k), Y)) (hAB : ∀ (p : P) (θ : ↑(TopCat.diskBoundary k)), B (p, 0, θ) = A (p, ⟨d • ↑θ.down, ⋯⟩)) {S : Set Y} (hA : ∀ (p : P) (v : ↑(Metric.closedBall 0 d)), ‖↑v‖ = 1 → A (p, v) ∈ S) (hB : ∀ (p : P) (θ : ↑(TopCat.diskBoundary k)), B (p, 1, θ) ∈ S) (p : P) {w : ↑(TopCat.disk k)} (hw : ‖↑w.down‖ = 1) : (discGlue hd A B hAB) (p, w) ∈ S

On the boundary sphere, a glued map takes values in a set containing the values of the inner piece on the unit sphere and of the outer piece on the outer circle s = 1.