The endgame: from the square extension to the relative Jordan–Schönflies theorem

This module carries the whole tail of the manuscript — prop:square-reduction, thm:closed-interior-extension, prop:pointed-extension, prop:exterior-extension and thm:main — parametrically over the square-extension interface.

Every theorem below takes Schoenflies.SquareExtension as an explicit hypothesis and assumes nothing else. In particular the standing hypothesis harc that older modules thread is discharged here at the call site, from Schoenflies.arc_complement in Schoenflies/JordanClosed.lean; it no longer appears in any signature. The implication proved by this module is

SquareExtension  ⟹  thm:main.

Schoenflies/JordanSchoenflies.lean supplies SquareExtension from the quantitative boundary construction and therefore closes this implication without an extra hypothesis.

What SquareExtension says

Schoenflies.SquareExtension is thm:square-extension written in the Schoenflies.IsHomeoOn style of Schoenflies/Inversion.lean: for every Jordan curve C and every restricted homeomorphism u : C → S (with named inverse v) there are maps F, G restricting to mutually inverse homeomorphisms between C ∪ Int(C) and Q, with F = u on C. Here S = Schoenflies.modelCurve and Q = Schoenflies.Plane.closedSquare 0 1; S = ∂Q is Schoenflies.modelCurve_eq_frontier, so this is literally the blueprint's Q = [-1,1]², S = ∂Q.

The chain

• prop:square-reduction is the blueprint's: pick a homeomorphism h : C' → S (lem:jordan-circle), extend h ∘ f and h to the square, and compose one with the inverse of the other. thm:closed-interior-extension is the same statement — under the standing assumption of SquareExtension the reduction is the theorem — and is recorded separately because everything downstream cites it by that name.
• prop:pointed-extension is the interesting one. Given the closed-interior extension Φ and a square chart Θ of the target disc, the two points Θ(Φ(a)) and Θ(b) are interior to Q, because Θ carries C' onto ∂Q and hence — being a bijection — Int(C') onto Q ∖ ∂Q. lem:square-point-mover then supplies a boundary-fixing self-homeomorphism M of Q moving the first to the second, and Θ⁻¹ ∘ M ∘ Θ ∘ Φ is the pointed extension: it agrees with Φ on C because M fixes ∂Q pointwise. This discharges Schoenflies.PointedInteriorExtension, the last hypothesis of prop:exterior-extension.
• thm:main is the closed pasting lemma applied twice, once to F and once to its inverse. The one point the blueprint leaves implicit is that the pasted map is injective: the interior extension carries Int(C) onto Int(C') and the exterior extension carries Ext(C) onto Ext(C'), so the two pieces cannot collide. Both facts are instances of Schoenflies.image_eq_diff_of_bijOn_union, which is the "a bijection matching one part of a partition matches the other part" principle.

The parametric construction interface

Within this deliberately parametric module, every conclusion depends on the Prop SquareExtension, so no def can produce the maps without an application of choice to that hypothesis. What is exported as data independently of the interface is Schoenflies.paste (the pasted map itself, with its two evaluation lemmas) and Schoenflies.IsHomeoOn.homeomorphOfUniv (the passage from a global IsHomeoOn to a genuine Plane ≃ₜ Plane). The theorems below return the maps in the unbundled ∃ F G, IsHomeoOn F G … shape of Schoenflies.exterior_extension, which composes.

Blueprint

• Schoenflies.SquareExtension — the thm:square-extension interface, discharged in Schoenflies/JordanSchoenflies.lean.
• Schoenflies.square_reduction — prop:square-reduction.
• Schoenflies.closed_interior_extension — thm:closed-interior-extension.
• Schoenflies.pointed_extension — prop:pointed-extension; it proves Schoenflies.PointedInteriorExtension of Schoenflies/Inversion.lean.
• Schoenflies.exterior_extension_of_squareExtension — prop:exterior-extension, restated with harc discharged and only SquareExtension left.
• Schoenflies.jordan_schoenflies_of_squareExtension, Schoenflies.jordan_schoenflies_homeomorph_of_squareExtension, Schoenflies.jordan_schoenflies_of_homeomorph_of_squareExtension — thm:main, the relative Jordan–Schönflies theorem, in the unbundled, the bundled, and the blueprint's own shape.

Supporting material with no blueprint statement, all general and all candidates for hoisting into the module that owns Schoenflies.IsHomeoOn: Schoenflies.exists_isHomeoOn_of_homeomorph, Schoenflies.IsHomeoOn.homeomorphOfUniv, Schoenflies.IsHomeoOn.image_inv_eq, Schoenflies.image_eq_diff_of_bijOn_union, Schoenflies.paste and Schoenflies.Plane.IsSquareMover.isHomeoOn.

Restricted homeomorphisms: three general tools

Schoenflies.IsHomeoOn (in Schoenflies/Inversion.lean) is the unbundled "restricts to a homeomorphism of S onto T". Three facts about it are needed below and are not there; they are general, and the section comment at IsHomeoOn already asks for the whole notion to be hoisted, so these should travel with it.

theorem Schoenflies.exists_isHomeoOn_of_homeomorph {S T : Set Plane} (e : ↑S ≃ₜ ↑T) : ∃ (f : Plane → Plane) (g : Plane → Plane), IsHomeoOn f g S T ∧ ∀ (z : Plane) (hz : z ∈ S), f z = ↑(e ⟨z, hz⟩)

A Homeomorph between two subsets of the plane can always be presented as an IsHomeoOn between honest self-maps of the plane: extend both by the identity.

This is the bridge from lem:jordan-circle, which produces Nonempty (↥C ≃ₜ ↥S), to the unbundled language everything downstream is written in.

noncomputable def Schoenflies.IsHomeoOn.homeomorphOfUniv {f g : Plane → Plane} (h : IsHomeoOn f g Set.univ Set.univ) : Plane ≃ₜ Plane

A restricted homeomorphism of the whole plane onto the whole plane is a homeomorphism. This is the last step of thm:main.

Equations

• h.homeomorphOfUniv = { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Schoenflies.IsHomeoOn.homeomorphOfUniv_apply {f g : Plane → Plane} (h : IsHomeoOn f g Set.univ Set.univ) (z : Plane) : h.homeomorphOfUniv z = f z

theorem Schoenflies.IsHomeoOn.image_inv_eq {f g : Plane → Plane} {S T : Set Plane} (h : IsHomeoOn f g S T) {A A' : Set Plane} (hA : A ⊆ S) (hA' : f '' A = A') : g '' A' = A

The inverse of a restricted homeomorphism undoes it on images: if f carries A ⊆ S onto A', then g carries A' back onto A.

theorem Schoenflies.image_eq_diff_of_bijOn_union {F : Plane → Plane} {A B T A' : Set Plane} (hF : Set.BijOn F (A ∪ B) T) (hA : F '' A = A') (hdisj : Disjoint A B) : F '' B = T \ A'

Matching one part of a partition matches the other. If F is a bijection of A ∪ B onto T carrying the disjoint piece A onto A', it carries B onto T ∖ A'.

Used three times below: Θ carries Int(C') onto Q ∖ ∂Q, and each of the interior and the exterior extension carries a region onto the corresponding region — which is exactly what makes the two pasted pieces of thm:main injective together.

The pasted map

thm:main glues the interior and the exterior extension. The glued map is Set.piecewise under a different name, spelled so that the two evaluation lemmas below are the only interface the proof needs.

noncomputable def Schoenflies.paste (S : Set Plane) (f₁ f₂ : Plane → Plane) : Plane → Plane

The map that is f₁ on S and f₂ off it. The blueprint's "defined by F_int on the closed interior and by F_ext on the closed exterior".

Equations

• Schoenflies.paste S f₁ f₂ z = if z ∈ S then f₁ z else f₂ z

theorem Schoenflies.paste_of_mem {S : Set Plane} {f₁ f₂ : Plane → Plane} {z : Plane} (hz : z ∈ S) : paste S f₁ f₂ z = f₁ z

theorem Schoenflies.paste_of_notMem {S : Set Plane} {f₁ f₂ : Plane → Plane} {z : Plane} (hz : z ∉ S) : paste S f₁ f₂ z = f₂ z

The square Q and its boundary S

The blueprint's Q = [-1,1]² is Plane.closedSquare 0 1 and its boundary S = ∂Q is modelCurve, by modelCurve_eq_frontier. One consequence is needed: removing the boundary from the closed square leaves the open square, which is where lem:square-point-mover wants its two points.

theorem Schoenflies.closedSquare_sdiff_modelCurve : Plane.closedSquare 0 1 \ modelCurve = Plane.openSquare 0 1

Q ∖ S = Q°.

theorem Schoenflies.Plane.IsSquareMover.isHomeoOn {c : Plane} {r : ℝ} {M N : Plane → Plane} (h : c.IsSquareMover r M N) : IsHomeoOn M N (c.closedSquare r) (c.closedSquare r)

A mover of the square, read as a restricted homeomorphism.

thm:square-extension, assumed

This is the one statement the module assumes, and the only thing standing between the library and thm:main. It is the last big theorem of the manuscript; its proof occupies the whole of Part II §§"Strongly accessible boundary points"–"Continuity at the Jordan curve".

def Schoenflies.SquareExtension : Prop

thm:square-extension (square extension), as a hypothesis: for every Jordan curve C and every homeomorphism u : C → S there is a homeomorphism C ∪ Int(C) → Q extending u.

Written in the unbundled Schoenflies.IsHomeoOn style: u comes with its inverse v, and the conclusion produces the extension F together with its inverse G. S is Schoenflies.modelCurve and Q is Schoenflies.Plane.closedSquare 0 1.

Equations

• One or more equations did not get rendered due to their size.

Disjointness of a curve from its two regions

A curve is disjoint from either of its two regions, and adding it and removing it again is the identity. The pastings below use these constantly.

theorem Schoenflies.disjoint_curve_inside (C : Set Plane) : Disjoint C (inside C)

theorem Schoenflies.disjoint_curve_outside (C : Set Plane) : Disjoint C (outside C)

theorem Schoenflies.union_inside_sdiff (C : Set Plane) : (C ∪ inside C) \ C = inside C

theorem Schoenflies.union_outside_sdiff (C : Set Plane) : (C ∪ outside C) \ C = outside C

theorem Schoenflies.image_inside_eq {C C' : Set Plane} {F G f : Plane → Plane} (hF : IsHomeoOn F G (C ∪ inside C) (C' ∪ inside C')) (hf : Set.EqOn F f C) (hfC : f '' C = C') : F '' inside C = inside C'

An extension of a boundary homeomorphism to the closed interiors carries the interior onto the interior. The blueprint never says this; the pointed extension and thm:main both need it.

theorem Schoenflies.image_outside_eq {C C' : Set Plane} {F G f : Plane → Plane} (hF : IsHomeoOn F G (C ∪ outside C) (C' ∪ outside C')) (hf : Set.EqOn F f C) (hfC : f '' C = C') : F '' outside C = outside C'

The same for the closed exteriors.

prop:square-reduction and thm:closed-interior-extension

The blueprint's proof verbatim: choose h : C' → S by lem:jordan-circle, extend h ∘ f and h over the two closed discs by thm:square-extension, and take Ψ⁻¹ ∘ Φ.

theorem Schoenflies.square_reduction {C C' : Set Plane} (hsq : SquareExtension) {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G (C ∪ inside C) (C' ∪ inside C') ∧ Set.EqOn F f C

prop:square-reduction (reduction to the square). If every boundary homeomorphism from a Jordan curve to S has a closed-interior extension, then every homeomorphism f : C → C' between Jordan curves extends to a homeomorphism C ∪ Int(C) → C' ∪ Int(C').

theorem Schoenflies.closed_interior_extension {C C' : Set Plane} (hsq : SquareExtension) {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G (C ∪ inside C) (C' ∪ inside C') ∧ Set.EqOn F f C

thm:closed-interior-extension (closed-interior extension). Every homeomorphism f : C → C' between Jordan curves extends to a homeomorphism of the closed interiors.

Under the standing assumption SquareExtension this is literally prop:square-reduction; it is recorded under its own name because everything downstream cites it by that name.

prop:pointed-extension

The blueprint's proof, with one step made explicit: the square chart Θ of the target disc carries Int(C') onto Q ∖ ∂Q = Q°, because it carries C' onto ∂Q and is a bijection of the closed disc onto Q. That is what puts the two points Θ(Φ(a)) and Θ(b) in the open square, where lem:square-point-mover lives.

theorem Schoenflies.pointed_extension (hsq : SquareExtension) : PointedInteriorExtension

prop:pointed-extension (pointed closed-interior extension). A boundary homeomorphism f : C → C' and prescribed points a ∈ Int(C), b ∈ Int(C') admit a closed-interior extension H with H(a) = b.

This is Schoenflies.PointedInteriorExtension, the hypothesis of Schoenflies.exterior_extension, discharged.

prop:exterior-extension, from the square extension

Schoenflies.exterior_extension in Schoenflies/Inversion.lean is proved already; it carries two hypotheses, the standing harc of thm:jordan and PointedInteriorExtension. Part I discharges the first (Schoenflies.arc_complement) and the previous theorem discharges the second, so only SquareExtension survives.

theorem Schoenflies.exterior_extension_of_squareExtension {C C' : Set Plane} (hsq : SquareExtension) {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G (C ∪ outside C) (C' ∪ outside C') ∧ Set.EqOn F f C

prop:exterior-extension (closed-exterior extension), with everything discharged but the square extension: every homeomorphism between two Jordan curves extends to a homeomorphism of their closed exteriors.

thm:main

The closed pasting lemma, twice. The blueprint's proof is three sentences; the two facts it leaves implicit are that the closed interior and the closed exterior are closed (they are the closures of the two regions, IsRegionOf.closure_eq) and that the pasted map is injective, which is image_inside_eq and image_outside_eq.

theorem Schoenflies.isClosed_union_inside {C : Set Plane} (hC : IsSeparating C) : IsClosed (C ∪ inside C)

The closed interior of a Jordan curve is closed: it is the closure of the interior.

theorem Schoenflies.isClosed_union_outside {C : Set Plane} (hC : IsSeparating C) : IsClosed (C ∪ outside C)

The closed exterior of a Jordan curve is closed.

theorem Schoenflies.union_inside_union_outside (C : Set Plane) : C ∪ inside C ∪ (C ∪ outside C) = Set.univ

The two closed sides cover the plane.

theorem Schoenflies.mem_outside_of_notMem_union_inside {C : Set Plane} {z : Plane} (hz : z ∉ C ∪ inside C) : z ∈ outside C

A point outside the closed interior is exterior.

theorem Schoenflies.jordan_schoenflies_of_squareExtension {C C' : Set Plane} (hsq : SquareExtension) {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G Set.univ Set.univ ∧ Set.EqOn F f C

thm:main, the relative Jordan–Schönflies theorem. Every homeomorphism between two Jordan curves extends to a homeomorphism of the whole plane.

This form takes Schoenflies.SquareExtension as its sole auxiliary theorem. It is the unbundled form; Schoenflies.jordan_schoenflies_homeomorph_of_squareExtension packages the result as a self-homeomorphism of the plane.

theorem Schoenflies.jordan_schoenflies_homeomorph_of_squareExtension {C C' : Set Plane} (hsq : SquareExtension) {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane ≃ₜ Plane), Set.EqOn (⇑F) f C

thm:main, with the extension packaged as a self-homeomorphism of the plane. This is the blueprint's statement: there is a homeomorphism F : ℝ² → ℝ² whose restriction to C is f.

theorem Schoenflies.jordan_schoenflies_of_homeomorph_of_squareExtension {C C' : Set Plane} (hsq : SquareExtension) (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (e : ↑C ≃ₜ ↑C') : ∃ (F : Plane ≃ₜ Plane), ∀ (z : ↑C), F ↑z = ↑(e z)

thm:main, taking the boundary homeomorphism in bundled form, which is how the blueprint states it: f : C → C' a homeomorphism of subspaces.