The attachment map for the protected extension

This module formalizes the metric input to the adjunction construction. The attachment set in M ⊕₁ ℝ is parametrized by M ⊕ Unit: the left summand is the base hyperplane and the right summand is the single elevated point.

@[reducible, inline]

abbrev ScottishBook155.OneSum (M : Type u) : Type u

The sum-norm product M ⊕₁ ℝ.

Equations

• ScottishBook155.OneSum M = WithLp 1 (M × ℝ)

noncomputable def ScottishBook155.attachmentPoint {M : Type u} (a : M) (H : ℝ) : M ⊕ Unit → OneSum M

Parametrization of the base hyperplane together with one elevated point.

Equations

• ScottishBook155.attachmentPoint a H (Sum.inl m) = WithLp.toLp 1 (m, 0)
• ScottishBook155.attachmentPoint a H (Sum.inr val) = WithLp.toLp 1 (a, H)

noncomputable def ScottishBook155.attachmentSet {M : Type u} (a : M) (H : ℝ) : Set (OneSum M)

The attachment subset of the sum-norm product.

Equations

• ScottishBook155.attachmentSet a H = Set.range (ScottishBook155.attachmentPoint a H)

def ScottishBook155.attachmentMap {M : Type u} {N : Type v} (V : M → N) (y : N) : M ⊕ Unit → N

The map prescribed on the attachment set before taking the metric adjunction.

Equations

• ScottishBook155.attachmentMap V y (Sum.inl m) = V m
• ScottishBook155.attachmentMap V y (Sum.inr val) = y

theorem ScottishBook155.dist_attachmentPoint_base_base {M : Type u} [NormedAddCommGroup M] (a m n : M) (H : ℝ) : dist (attachmentPoint a H (Sum.inl m)) (attachmentPoint a H (Sum.inl n)) = dist m n

theorem ScottishBook155.dist_attachmentPoint_base_top {M : Type u} [NormedAddCommGroup M] (a m : M) {H : ℝ} (hH : 0 ≤ H) : dist (attachmentPoint a H (Sum.inl m)) (attachmentPoint a H (Sum.inr ())) = dist m a + H

theorem ScottishBook155.attachmentSet_eq {M : Type u} (a : M) (H : ℝ) : attachmentSet a H = {x : OneSum M | WithLp.snd x = 0} ∪ {WithLp.toLp 1 (a, H)}

theorem ScottishBook155.isClosed_attachmentSet {M : Type u} [NormedAddCommGroup M] (a : M) (H : ℝ) : IsClosed (attachmentSet a H)

The attachment set is closed in M ⊕₁ ℝ.

theorem ScottishBook155.attachmentPoint_mem_attachmentSet {M : Type u} (a : M) (H : ℝ) (p : M ⊕ Unit) : attachmentPoint a H p ∈ attachmentSet a H

theorem ScottishBook155.dist_to_attachmentBase {M : Type u} [NormedAddCommGroup M] (a m : M) (H s : ℝ) : dist (WithLp.toLp 1 (m, s)) (attachmentPoint a H (Sum.inl m)) = |s|

theorem ScottishBook155.infDist_attachmentSet_le_abs {M : Type u} [NormedAddCommGroup M] (a m : M) (H s : ℝ) : Metric.infDist (WithLp.toLp 1 (m, s)) (attachmentSet a H) ≤ |s|

The vertical route to the base hyperplane gives the elementary upper bound on distance to the attachment set used in the collar argument.

theorem ScottishBook155.infDist_attachmentSet_eq_min {M : Type u} [NormedAddCommGroup M] (a m : M) (H s : ℝ) : Metric.infDist (WithLp.toLp 1 (m, s)) (attachmentSet a H) = min |s| (dist m a + |s - H|)

Exact distance from a point to the union of the base hyperplane and the single elevated attachment point.

theorem ScottishBook155.abs_add_abs_lt_dist_of_infDist_add_lt {M : Type u} [NormedAddCommGroup M] (a m₀ m₁ : M) {H r s₀ s₁ : ℝ} (hr : 0 < r) (hH : 2 * r < H) (hd : dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁)) ≤ r) (hfar : Metric.infDist (WithLp.toLp 1 (m₀, s₀)) (attachmentSet a H) + Metric.infDist (WithLp.toLp 1 (m₁, s₁)) (attachmentSet a H) < dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁))) : |s₀| + |s₁| < dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁))

In the complementary two-point case, a height above 2r forces both nearest attachment routes to use the base hyperplane.

theorem ScottishBook155.abs_lt_of_infDist_add_lt {M : Type u} [NormedAddCommGroup M] (a m₀ m₁ : M) {H r s₀ s₁ : ℝ} (hr : 0 < r) (hH : 2 * r < H) (hd : dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁)) ≤ r) (hfar : Metric.infDist (WithLp.toLp 1 (m₀, s₀)) (attachmentSet a H) + Metric.infDist (WithLp.toLp 1 (m₁, s₁)) (attachmentSet a H) < dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁))) : |s₀| < r ∧ |s₁| < r

theorem ScottishBook155.attachmentPoint_injective {M : Type u} (a : M) {H : ℝ} (hH : H ≠ 0) : Function.Injective (attachmentPoint a H)

theorem ScottishBook155.attachmentMap_injective {M : Type u} {N : Type v} {V : M → N} {y : N} (hV : Function.Injective V) (hy : y ∉ Set.range V) : Function.Injective (attachmentMap V y)

theorem ScottishBook155.attachmentMap_dist_le {M : Type u} [NormedAddCommGroup M] {N : Type v} [PseudoMetricSpace N] {V : M → N} (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (a : M) (y : N) {H : ℝ} (hgap : dist (V a) y < H) (p q : M ⊕ Unit) : dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)

The prescribed attachment map is nonexpansive with respect to the ambient sum-norm distance on its parametrized attachment set.