A continuous injection between two arcs is monotone

Two parametrizations f and f' of two arcs, and a continuous injection g carrying the first arc onto the second. Then g respects the order in which the two parametrizations traverse their arcs: the composite parameter map

s ↦ (the parameter at which f' sits at g (f s))

is strictly monotone on [0, 1] — increasing or decreasing according to whether g matches the two parametrizations' starting points or swaps them. Consequently g carries a subarc of the first arc onto a subarc of the second, with the corresponding parameters.

That last sentence is what every consumer wants, and it is ArcMatch.image_image_uIcc:

g '' (f '' uIcc s u) = f' '' uIcc (transferParam f f' g s) (transferParam f f' g u).

Stated over uIcc, it is orientation-free: uIcc is unordered, so the identity holds whether the transfer map increases or decreases, and a consumer that does not know which way round its two parametrizations run does not have to find out. Only the two corollaries about initial and terminal subarcs (image_initial, image_terminal) need the matching-endpoint hypothesis, and they take it explicitly.

How the parameter map is built

No inverse parametrization is constructed as a continuous map. arcParam f' p picks, by choice, a parameter in [0, 1] sitting at p; injectivity of f' makes it the parameter, and its continuity along the composite is proved by hand from Schoenflies.exists_ball_inter_subset_image — the statement, already on main, that a parametrization is an open map onto its arc. That is exactly the continuity of the inverse, in the only form needed here, and it avoids constructing a homeomorphism ↥I ≃ₜ ↥A and pushing it through subtype coercions.

With the composite continuous and injective on [0, 1], Mathlib's ContinuousOn.strictMonoOn_of_injOn_Icc' supplies the monotone-or-antitone dichotomy.

Blueprint

There is no blueprint statement for this. The manuscript uses it silently, in two places:

• def:matched-pair, clause 3 — "on each corresponding pair of edges, g restricts to a fixed chosen homeomorphism between them, matching endpoints". When an edge is subdivided, the two halves of that homeomorphism have to be the chosen homeomorphisms of the two new edges; that they are half-arc-to-half-arc, rather than merely arc-to-arc, is this file.
• def:generated-structure, operation 1 (edge subdivision) — "the corresponding point is inserted into the corresponding edge using the edge parametrization". "Corresponding" is the transfer map below, and the sentence's content is that inserting corresponding points splits the edge homeomorphism into two edge homeomorphisms.

Declarations:

• Schoenflies.arcParam — the parameter of a point on a parametrized arc.
• Schoenflies.ArcMatch — the hypothesis bundle: two parametrized arcs and a continuous injection of the first onto the second.
• Schoenflies.transferParam — the induced map on parameters.
• Schoenflies.ArcMatch.continuousOn_param, …injOn_param, …strictMonoOn_or_strictAntiOn_param — the monotonicity.
• Schoenflies.ArcMatch.image_image_uIcc, …image_subarc — the orientation-free conclusion.
• Schoenflies.ArcMatch.image_initial, …image_terminal — initial and terminal subarcs, given matching endpoints.

The parameter of a point on a parametrized arc

noncomputable def Schoenflies.arcParam (f : ℝ → Plane) (p : Plane) : ℝ

The parameter in [0, 1] at which f sits at p, chosen; junk (0) when there is none.

Only ever used under an injectivity hypothesis, which makes the choice unique (arcParam_eq_of_apply).

Equations

• Schoenflies.arcParam f p = if h : ∃ s ∈ unitInterval, f s = p then h.choose else 0

theorem Schoenflies.arcParam_spec {f : ℝ → Plane} {p : Plane} (hp : p ∈ f '' unitInterval) : arcParam f p ∈ unitInterval ∧ f (arcParam f p) = p

theorem Schoenflies.arcParam_mem_I {f : ℝ → Plane} {p : Plane} (hp : p ∈ f '' unitInterval) : arcParam f p ∈ unitInterval

theorem Schoenflies.apply_arcParam {f : ℝ → Plane} {p : Plane} (hp : p ∈ f '' unitInterval) : f (arcParam f p) = p

theorem Schoenflies.arcParam_eq_of_apply {f : ℝ → Plane} {p : Plane} {s : ℝ} (hi : Set.InjOn f unitInterval) (hs : s ∈ unitInterval) (hfs : f s = p) : arcParam f p = s

Under injectivity the chosen parameter is the only one.

The hypothesis bundle

structure Schoenflies.ArcMatch (f f' : ℝ → Plane) (g : Plane → Plane) : Prop

Two parametrized arcs and a continuous injection of the first onto the second.

A Prop-valued bundle rather than seven separate hypotheses: every theorem below needs most of them, and a consumer assembles it once.

• continuousOn_src : ContinuousOn f unitInterval

  The source parametrization is continuous.

• injOn_src : Set.InjOn f unitInterval

  …and injective.

• continuousOn_tgt : ContinuousOn f' unitInterval

  The target parametrization is continuous.

• injOn_tgt : Set.InjOn f' unitInterval

  …and injective.

• continuousOn_map : ContinuousOn g (f '' unitInterval)

  The map is continuous on the source arc.

• injOn_map : Set.InjOn g (f '' unitInterval)

  …and injective on it.

• image_eq : g '' f '' unitInterval = f' '' unitInterval

  …and carries the source arc onto the target arc.

noncomputable def Schoenflies.transferParam (f f' : ℝ → Plane) (g : Plane → Plane) : ℝ → ℝ

The map g induces on parameters: send s to the parameter at which f' sits at g (f s).

A plain def, not depending on the ArcMatch proof, so that a consumer can name the target parameter before it has assembled the hypotheses — which is exactly what Schoenflies/RealizeSubdivHomeo.lean does.

Equations

• Schoenflies.transferParam f f' g s = Schoenflies.arcParam f' (g (f s))

theorem Schoenflies.ArcMatch.mem_image_map {f f' : ℝ → Plane} {g : Plane → Plane} {s : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) : g (f s) ∈ f' '' unitInterval

theorem Schoenflies.ArcMatch.param_mem_I {f f' : ℝ → Plane} {g : Plane → Plane} {s : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) : transferParam f f' g s ∈ unitInterval

theorem Schoenflies.ArcMatch.apply_param {f f' : ℝ → Plane} {g : Plane → Plane} {s : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) : f' (transferParam f f' g s) = g (f s)

The defining property: the target parametrization at the transferred parameter is the image of the source parametrization.

theorem Schoenflies.ArcMatch.param_eq {f f' : ℝ → Plane} {g : Plane → Plane} {s u : ℝ} (h : ArcMatch f f' g) (hu : u ∈ unitInterval) (heq : f' u = g (f s)) : transferParam f f' g s = u

The transferred parameter is characterized, not merely chosen.

theorem Schoenflies.ArcMatch.injOn_param {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) : Set.InjOn (transferParam f f' g) unitInterval

theorem Schoenflies.ArcMatch.continuousOn_param {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) : ContinuousOn (transferParam f f' g) unitInterval

The transfer map is continuous. This is the continuity of the inverse parametrization f'⁻¹, in the only form needed, and it is proved from the fact that a parametrization is an open map onto its arc: a prescribed parameter window around transferParam f f' g s pulls back to a ball around g (f s), and continuity of g ∘ f turns that into a parameter window around s.

theorem Schoenflies.ArcMatch.strictMonoOn_or_strictAntiOn_param {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) : StrictMonoOn (transferParam f f' g) unitInterval ∨ StrictAntiOn (transferParam f f' g) unitInterval

The transfer map is strictly monotone, in one direction or the other. Which one is decided by the endpoints; every conclusion below that does not mention an endpoint holds in both cases.

theorem Schoenflies.ArcMatch.surjOn_param {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) : unitInterval ⊆ transferParam f f' g '' unitInterval

Every target parameter is hit. g is onto the target arc and f' parametrizes it, so the transfer map is onto [0, 1] — this is where image_eq earns its keep.

theorem Schoenflies.ArcMatch.image_param_I {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) : transferParam f f' g '' unitInterval = unitInterval

The transfer map is a bijection of the parameter interval.

The image of a parameter interval

theorem Schoenflies.ArcMatch.param_mem_uIcc {f f' : ℝ → Plane} {g : Plane → Plane} {s u : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) (hu : u ∈ unitInterval) {x : ℝ} (hx : x ∈ Set.uIcc s u) : transferParam f f' g x ∈ Set.uIcc (transferParam f f' g s) (transferParam f f' g u)

theorem Schoenflies.ArcMatch.image_param_uIcc {f f' : ℝ → Plane} {g : Plane → Plane} {s u : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) (hu : u ∈ unitInterval) : transferParam f f' g '' Set.uIcc s u = Set.uIcc (transferParam f f' g s) (transferParam f f' g u)

The transfer map carries a parameter interval onto the corresponding one. Stated over uIcc, so it is indifferent to the direction of either traversal.

theorem Schoenflies.ArcMatch.image_image_uIcc {f f' : ℝ → Plane} {g : Plane → Plane} {s u : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) (hu : u ∈ unitInterval) : g '' f '' Set.uIcc s u = f' '' Set.uIcc (transferParam f f' g s) (transferParam f f' g u)

The map carries a subarc onto the corresponding subarc. The form every consumer wants, and the reason for this file.

theorem Schoenflies.ArcMatch.image_subarc {f f' : ℝ → Plane} {g : Plane → Plane} {s u : ℝ} (h : ArcMatch f f' g) (hs : s ∈ unitInterval) (hu : u ∈ unitInterval) : g '' subarc f s u '' unitInterval = subarc f' (transferParam f f' g s) (transferParam f f' g u) '' unitInterval

The same in the vocabulary of Schoenflies/Subarc.lean.

Matching endpoints

theorem Schoenflies.ArcMatch.param_zero {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) (h0 : g (f 0) = f' 0) : transferParam f f' g 0 = 0

theorem Schoenflies.ArcMatch.strictMonoOn_param {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) (h0 : g (f 0) = f' 0) : StrictMonoOn (transferParam f f' g) unitInterval

With the starting points matched the transfer map increases. If it decreased, the whole interval would map below transferParam f f' g 0 = 0, which is impossible since transferred parameters lie in [0, 1].

theorem Schoenflies.ArcMatch.param_one {f f' : ℝ → Plane} {g : Plane → Plane} (h : ArcMatch f f' g) (h0 : g (f 0) = f' 0) : transferParam f f' g 1 = 1

theorem Schoenflies.ArcMatch.image_initial {f f' : ℝ → Plane} {g : Plane → Plane} {u : ℝ} (h : ArcMatch f f' g) (h0 : g (f 0) = f' 0) (hu : u ∈ unitInterval) : g '' f '' Set.Icc 0 u = f' '' Set.Icc 0 (transferParam f f' g u)

Initial subarcs correspond.

theorem Schoenflies.ArcMatch.image_terminal {f f' : ℝ → Plane} {g : Plane → Plane} {u : ℝ} (h : ArcMatch f f' g) (h0 : g (f 0) = f' 0) (hu : u ∈ unitInterval) : g '' f '' Set.Icc u 1 = f' '' Set.Icc (transferParam f f' g u) 1

Terminal subarcs correspond.

theorem Schoenflies.ArcMatch.param_mem_Ioo {f f' : ℝ → Plane} {g : Plane → Plane} {u : ℝ} (h : ArcMatch f f' g) (h0 : g (f 0) = f' 0) (hu : u ∈ Set.Ioo 0 1) : transferParam f f' g u ∈ Set.Ioo 0 1

An interior parameter transfers to an interior parameter.

theorem Schoenflies.ArcMatch.param_mem_Ioo_of_ends {f f' : ℝ → Plane} {g : Plane → Plane} {u : ℝ} (h : ArcMatch f f' g) (hends : transferParam f f' g 0 = 0 ∧ transferParam f f' g 1 = 1 ∨ transferParam f f' g 0 = 1 ∧ transferParam f f' g 1 = 0) (hu : u ∈ Set.Ioo 0 1) : transferParam f f' g u ∈ Set.Ioo 0 1

An interior parameter transfers to an interior parameter, without assuming which way the two parametrizations run: the two endpoints go to the two endpoints in one order or the other, and strict monotonicity keeps the inside inside.