The nonlinear retraction of the metric adjunction

The flat source retraction agrees with the attachment map. Together with the identity on the old target it is nonexpansive for the adjunction predistance, so it descends through metric separation.

noncomputable def ScottishBook155.sourceRetractionOne {M : Type u} {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (x : OneSum M) : N

The source retraction expressed on the one-sum model of the source and its added real coordinate.

Equations

• ScottishBook155.sourceRetractionOne V a y L H x = ScottishBook155.sourceRetraction V a y L H (WithLp.fst x) (WithLp.snd x)

noncomputable def ScottishBook155.adjunctionRetractionPre {M : Type u} {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) : OneSum M ⊕ N → N

The map on the disjoint union that retracts the source component and fixes the target component.

Equations

• ScottishBook155.adjunctionRetractionPre V a y L H (Sum.inl x_1) = ScottishBook155.sourceRetractionOne V a y L H x_1
• ScottishBook155.adjunctionRetractionPre V a y L H (Sum.inr n) = n

theorem ScottishBook155.sourceRetractionOne_attachment {M : Type u} {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) (p : M ⊕ Unit) : sourceRetractionOne V a y L H (attachmentPoint a H p) = attachmentMap V y p

theorem ScottishBook155.sourceRetractionOne_dist_le {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (x z : OneSum M) : dist (sourceRetractionOne V a y L H x) (sourceRetractionOne V a y L H z) ≤ dist x z

theorem ScottishBook155.sourceRetractionOne_dist_le_excursionCost {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (x₀ x₁ : OneSum M) : dist (sourceRetractionOne V a y L H x₀) (sourceRetractionOne V a y L H x₁) ≤ attachmentExcursionCost V a y H x₀ x₁

theorem ScottishBook155.sourceRetractionOne_dist_le_sourceAdjunctionDist {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (x₀ x₁ : OneSum M) : dist (sourceRetractionOne V a y L H x₀) (sourceRetractionOne V a y L H x₁) ≤ sourceAdjunctionDist V a y H x₀ x₁

theorem ScottishBook155.sourceRetractionOne_dist_le_attachmentTargetCost {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (x : OneSum M) (n : N) : dist (sourceRetractionOne V a y L H x) n ≤ attachmentTargetCost V a y H x n

theorem ScottishBook155.adjunctionRetractionPre_dist_le {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (z w : OneSum M ⊕ N) : dist (adjunctionRetractionPre V a y L H z) (adjunctionRetractionPre V a y L H w) ≤ adjunctionPreDist V a y H z w

noncomputable def ScottishBook155.adjunctionRetraction {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) : AdjunctionSpace V a y H hattach → N

The pointed nonexpansive retraction from the metric adjunction to the old target.

Equations

• ScottishBook155.adjunctionRetraction V a y L H hattach hLH hL hV hgap = id (SeparationQuotient.lift (ScottishBook155.adjunctionRetractionPre V a y L H) ⋯)

theorem ScottishBook155.adjunctionRetraction_source {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (x : OneSum M) : adjunctionRetraction V a y L H hattach hLH hL hV hgap (adjunctionSourceMk V a y H hattach x) = sourceRetractionOne V a y L H x

theorem ScottishBook155.adjunctionRetraction_target {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (n : N) : adjunctionRetraction V a y L H hattach hLH hL hV hgap (adjunctionTargetMk V a y H hattach n) = n

theorem ScottishBook155.adjunctionRetraction_dist_le {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (p q : AdjunctionSpace V a y H hattach) : dist (adjunctionRetraction V a y L H hattach hLH hL hV hgap p) (adjunctionRetraction V a y L H hattach hLH hL hV hgap q) ≤ dist p q

The descended retraction is nonexpansive for the metric-quotient distance.