Jordan curves

A Jordan curve — a simple closed curve — is a subset of a topological space homeomorphic to the circle. This file introduces the predicate TauCeti.IsJordanCurve and its basic API.

The circle is Mathlib's Circle, the unit circle of ℂ as a topological group; the notion itself is purely topological, so TauCeti.IsJordanCurve is stated for a subset of an arbitrary topological space. ℂ is mentioned only by the two concrete curves towards the end of the file: the model curve, a circle Metric.sphere c r of positive radius, and the frontier of a bounded convex set with nonempty interior. The model is built from the complex affine change of coordinates w ↦ (w - c) / r, so it uses the field structure of ℂ and not only its metric, and the convex frontier is obtained from the model by transport.

Phrasing the predicate as the set is homeomorphic to the circle, rather than the set is the range of a continuous map on [0, 1] that is injective except for matching endpoints, is what makes it usable: over a Hausdorff ambient space the two agree, because there a continuous injection out of a compact space is an embedding, but the parametrized form buries that argument in every use. Passing from a parametrization to the predicate is TauCeti.IsJordanCurve.image, which turns a continuous injective map defined on a set already known to be a Jordan curve — a circle in ℂ, say — into a proof that its image is one; TauCeti.IsJordanCurve.of_image runs the other way, transporting the property back to a compact set from an image already known to be a Jordan curve.

Main definitions

• TauCeti.IsJordanCurve — a set homeomorphic to the circle.
• TauCeti.jordanParam — the parametrization of a Jordan curve by the circle underlying a homeomorphism of the curve with Circle.

Main results

• TauCeti.IsJordanCurve.isCompact, TauCeti.IsJordanCurve.isPathConnected, TauCeti.IsJordanCurve.nonempty and TauCeti.IsJordanCurve.not_subsingleton — a Jordan curve is a nonempty compact path-connected set with more than one point.
• TauCeti.IsJordanCurve.image and TauCeti.IsJordanCurve.of_image — being a Jordan curve transfers in both directions along a map that is continuous and injective on the set, provided the codomain is Hausdorff (and, in the direction that transports the property back from the image, the source set is known to be compact).
• TauCeti.IsJordanCurve.image_homeomorph and TauCeti.isJordanCurve_image_homeomorph_iff — being a Jordan curve is invariant under a homeomorphism of the ambient spaces; no separation axiom is needed.
• TauCeti.continuous_jordanParam, TauCeti.jordanParam_injective, TauCeti.isInducing_jordanParam, TauCeti.range_jordanParam, TauCeti.jordanParam_apply and TauCeti.jordanParam_apply_apply — the parametrization of a Jordan curve by the circle is a continuous injection, is inducing, traces out exactly the curve, and undoes e; this is what carries a statement about the circle to one about an arbitrary Jordan curve.
• TauCeti.sphereCircleHomeomorph and TauCeti.isJordanCurve_sphere — a circle of positive radius in ℂ is a Jordan curve, by the affine change of coordinates w ↦ (w - c) / r.
• TauCeti.isJordanCurve_frontier_of_convex — the frontier of a bounded convex subset of ℂ with nonempty interior is a Jordan curve. This is TauCeti.isJordanCurve_sphere with the disc weakened to an arbitrary convex body, the affine change of coordinates being replaced by Mathlib's gauge rescaling.
• TauCeti.locallyConnectedSpace_sphere and TauCeti.IsJordanCurve.locallyConnectedSpace — a circle in ℂ, and hence every Jordan curve, is locally connected.

Motivation

This is the vocabulary layer L5 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) is stated in: its milestone, the Carathéodory boundary correspondence, is about the Riemann map of a Jordan domain, and the roadmap records that the pinned Mathlib has no Jordan-curve vocabulary to state it against. The complex-analytic half — Jordan domains, the discs among them, and the boundary of a domain that a conformal map carries onto a disc — is in TauCeti/Analysis/Complex/Conformal/Jordan/Domain.lean.

Local connectedness of a Jordan curve is what that milestone needs of the hypothesis side: the route to the extension theorem for a Jordan domain Ω runs through Carathéodory's continuity theorem, whose hypothesis is that frontier Ω be locally connected, and TauCeti.IsJordanCurve.locallyConnectedSpace is what discharges it (as TauCeti.IsJordanDomain.locallyConnectedSpace_frontier). Mathlib knows the circle is compact, connected and path connected, but records no local connectedness for it, and the property is not preserved by continuous images, so it is proved here from TauCeti.locallyConnectedSpace_image_of_isCompact.

References

• C. Jordan, Cours d'analyse de l'École Polytechnique, vol. 3 (1887).
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.

def TauCeti.IsJordanCurve {X : Type u_1} [TopologicalSpace X] (C : Set X) : Prop

A Jordan curve, or simple closed curve, in a topological space: a subset homeomorphic to the circle.

The predicate is Nonempty (C ≃ₜ Circle) rather than a chosen homeomorphism, so that it is a Prop; TauCeti.isJordanCurve_iff recovers the homeomorphism from another module, where the definition itself is not exposed.

Equations

• TauCeti.IsJordanCurve C = Nonempty (↑C ≃ₜ Circle)

theorem TauCeti.isJordanCurve_iff {X : Type u_1} [TopologicalSpace X] {C : Set X} : IsJordanCurve C ↔ Nonempty (↑C ≃ₜ Circle)

A set is a Jordan curve exactly when it is homeomorphic to the circle. This is the interface to TauCeti.IsJordanCurve outside its defining module.

theorem TauCeti.IsJordanCurve.isCompact {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) : IsCompact C

A Jordan curve is compact: the circle is.

theorem TauCeti.IsJordanCurve.isClosed {X : Type u_1} [TopologicalSpace X] {C : Set X} [T2Space X] (h : IsJordanCurve C) : IsClosed C

A Jordan curve in a Hausdorff space is closed.

theorem TauCeti.IsJordanCurve.isPathConnected {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) : IsPathConnected C

A Jordan curve is path connected: the circle is.

theorem TauCeti.IsJordanCurve.isConnected {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) : IsConnected C

A Jordan curve is connected.

theorem TauCeti.IsJordanCurve.nonempty {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) : C.Nonempty

A Jordan curve is nonempty.

theorem TauCeti.IsJordanCurve.not_subsingleton {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) : ¬C.Subsingleton

A Jordan curve has more than one point: the circle contains both 1 and -1. Together with TauCeti.IsJordanCurve.isConnected this rules out the degenerate curves, so a Jordan curve is a nondegenerate continuum.

theorem TauCeti.IsJordanCurve.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} [T2Space Y] (h : IsJordanCurve C) {g : X → Y} (hg : ContinuousOn g C) (hgi : Set.InjOn g C) : IsJordanCurve (g '' C)

A Jordan curve is carried to a Jordan curve by a continuous injection. Only continuity and injectivity on the curve are needed, the curve supplying the compactness that upgrades them to a homeomorphism onto the image.

theorem TauCeti.IsJordanCurve.of_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} [T2Space Y] (hC : IsCompact C) {g : X → Y} (hg : ContinuousOn g C) (hgi : Set.InjOn g C) (h : IsJordanCurve (g '' C)) : IsJordanCurve C

A compact set carried onto a Jordan curve by a continuous injection is a Jordan curve. This is the converse of TauCeti.IsJordanCurve.image; compactness of the source has to be assumed here, since it is no longer inherited from the curve. It is the form in which the predicate is verified when the curve is the unknown rather than the parameter: one exhibits a continuous injective map of the set onto a set already known to be a Jordan curve, as the boundary correspondence does with the boundary of a disc.

theorem TauCeti.IsJordanCurve.image_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} (h : IsJordanCurve C) (e : X ≃ₜ Y) : IsJordanCurve (⇑e '' C)

The image of a Jordan curve under a homeomorphism of the ambient spaces is a Jordan curve. Unlike TauCeti.IsJordanCurve.image this needs no separation axiom on the codomain, because Homeomorph.image supplies the homeomorphism onto the image outright.

@[simp]

theorem TauCeti.isJordanCurve_image_homeomorph_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} (e : X ≃ₜ Y) : IsJordanCurve (⇑e '' C) ↔ IsJordanCurve C

Being a Jordan curve is invariant under a homeomorphism of the ambient spaces. This is the characteristic form of TauCeti.IsJordanCurve.image_homeomorph: the backward direction is that lemma applied to e.symm, which no consumer then has to spell out.

The parametrization by the circle

Every transport of a statement about Circle to a Jordan curve goes through the parametrization jordanParam e attached to a homeomorphism e, so its properties — continuity, injectivity, range, and that it is inducing — are collected here rather than rebuilt at each use, both by the cutting of a curve at one or two of its points (TauCeti/Topology/JordanCurve/Separation.lean) and by the quantitative form of that cutting (TauCeti/Topology/JordanCurve/SmallArc.lean).

noncomputable def TauCeti.jordanParam {X : Type u_1} [TopologicalSpace X] {C : Set X} (e : ↑C ≃ₜ Circle) : Circle → X

The parametrization of a Jordan curve by the circle underlying a homeomorphism e: the composite of e.symm with the inclusion of the curve into the ambient space.

Equations

• TauCeti.jordanParam e u = ↑(e.symm u)

theorem TauCeti.continuous_jordanParam {X : Type u_1} [TopologicalSpace X] {C : Set X} (e : ↑C ≃ₜ Circle) : Continuous (jordanParam e)

The parametrization TauCeti.jordanParam of a Jordan curve by the circle is continuous.

theorem TauCeti.jordanParam_injective {X : Type u_1} [TopologicalSpace X] {C : Set X} (e : ↑C ≃ₜ Circle) : Function.Injective (jordanParam e)

The parametrization TauCeti.jordanParam of a Jordan curve by the circle is injective: this is the simplicity of the curve.

theorem TauCeti.isInducing_jordanParam {X : Type u_1} [TopologicalSpace X] {C : Set X} (e : ↑C ≃ₜ Circle) : Topology.IsInducing (jordanParam e)

The parametrization TauCeti.jordanParam of a Jordan curve by the circle is inducing, so preconnectedness of a subset of the curve may be tested on its preimage of parameters.

@[simp]

theorem TauCeti.range_jordanParam {X : Type u_1} [TopologicalSpace X] {C : Set X} (e : ↑C ≃ₜ Circle) : Set.range (jordanParam e) = C

The parametrization TauCeti.jordanParam of a Jordan curve by the circle traces out exactly the curve.

@[simp]

theorem TauCeti.jordanParam_apply {X : Type u_1} [TopologicalSpace X] {C : Set X} (e : ↑C ≃ₜ Circle) (u : Circle) : jordanParam e u = ↑(e.symm u)

The defining equation of TauCeti.jordanParam: the parameter u names the point e.symm u of the curve, read in the ambient space. This is the general application lemma, so a consumer never has to unfold the definition.

theorem TauCeti.jordanParam_apply_apply {X : Type u_1} [TopologicalSpace X] {C : Set X} {p : X} (e : ↑C ≃ₜ Circle) (hp : p ∈ C) : jordanParam e (e ⟨p, hp⟩) = p

The parametrization TauCeti.jordanParam of a Jordan curve by the circle undoes e: it sends the parameter e ⟨p, hp⟩ of a point p of the curve back to p. Simp proves this from TauCeti.jordanParam_apply; it is stated for the rw steps that produce the point p itself rather than a coerced parameter.

The model curve: a circle in ℂ

noncomputable def TauCeti.sphereCircleHomeomorph {r : ℝ} (c : ℂ) (hr : 0 < r) : ↑(Metric.sphere c r) ≃ₜ Circle

The affine parametrization w ↦ (w - c) / r of a circle of centre c and positive radius r in ℂ by the unit circle. It is the restriction to the spheres of the inverse of Mathlib's ambient affineHomeomorph r c, so only the membership equivalence is proved here.

Equations

• TauCeti.sphereCircleHomeomorph c hr = ((affineHomeomorph (↑r) c ⋯).symm.subtype ⋯).trans TauCeti.unitSphereCircleHomeomorph✝

@[simp]

theorem TauCeti.coe_sphereCircleHomeomorph_apply {r : ℝ} (c : ℂ) (hr : 0 < r) (w : ↑(Metric.sphere c r)) : ↑((sphereCircleHomeomorph c hr) w) = (↑w - c) / ↑r

The parametrization of sphere c r by the unit circle divides out the affine change of coordinates.

@[simp]

theorem TauCeti.coe_sphereCircleHomeomorph_symm_apply {r : ℝ} (c : ℂ) (hr : 0 < r) (z : Circle) : ↑((sphereCircleHomeomorph c hr).symm z) = c + ↑r * ↑z

The inverse parametrization of sphere c r by the unit circle is the affine change of coordinates.

theorem TauCeti.isJordanCurve_sphere {r : ℝ} (c : ℂ) (hr : 0 < r) : IsJordanCurve (Metric.sphere c r)

A circle of positive radius in ℂ is a Jordan curve.

theorem TauCeti.isJordanCurve_frontier_of_convex {s : Set ℂ} (hs : Convex ℝ s) (hne : (interior s).Nonempty) (hb : Bornology.IsBounded s) : IsJordanCurve (frontier s)

The frontier of a bounded convex subset of ℂ with nonempty interior is a Jordan curve.

This is TauCeti.isJordanCurve_sphere with the disc weakened to an arbitrary convex body, which it recovers at s = Metric.ball c r. The model curve transports because Mathlib's gauge rescaling supplies an ambient homeomorphism e : ℂ ≃ₜ ℂ carrying frontier s onto the unit circle (exists_homeomorph_image_interior_closure_frontier_eq_unitBall), so the affine change of coordinates above is simply replaced by a nonlinear one and no further topology is needed.

The set is asked neither to be open nor to be nonempty: what a convex set needs in order to have a one-dimensional frontier is that it be solid, and that is (interior s).Nonempty. Without it the statement fails — a segment is convex and bounded, and is its own frontier.

Local connectedness

instance TauCeti.locallyConnectedSpace_sphere (c : ℂ) (r : ℝ) : LocallyConnectedSpace ↑(Metric.sphere c r)

A circle in ℂ is locally connected. It is the image of the compact interval [-π, π], which is convex and hence locally connected, under the continuous θ ↦ c + r * exp (θ * I), so TauCeti.locallyConnectedSpace_image_of_isCompact applies. A sphere of negative radius is empty, and vacuously locally connected.

instance TauCeti.locallyConnectedSpace_circle : LocallyConnectedSpace Circle

The circle is locally connected. Circle is the unit circle of ℂ, so this is the unit case of TauCeti.locallyConnectedSpace_sphere transported along TauCeti.sphereCircleHomeomorph. Mathlib records the circle as compact, connected and path connected, but not as locally connected.

theorem TauCeti.IsJordanCurve.locallyConnectedSpace {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) : LocallyConnectedSpace ↑C

A Jordan curve is locally connected, being homeomorphic to the circle.

This is the form in which the hypothesis of Carathéodory's continuity theorem — that the boundary of the domain be locally connected — is met by a Jordan domain, which is what layer L5 of the conformal-mapping roadmap is about; see TauCeti.IsJordanDomain.locallyConnectedSpace_frontier.