A proper subcontinuum of a Jordan curve is an arc #
TauCeti/Topology/JordanCurve/Separation.lean cuts a Jordan curve at one or two given points.
This file describes the pieces from the other side: it classifies the compact connected subsets of
a Jordan curve. Every one of them other than the curve itself is a point or an arc — the range
of an injective path — and its complement in the curve is again path connected. In particular a
compact connected subset that is nowhere dense in the curve is a subsingleton, hence a single
point as soon as it is nonempty, which is the form in which the classification is spent.
The argument #
Everything is transported from the model curve Circle, so the work is on the circle, and the
transport is the parametrization TauCeti.jordanParam of TauCeti/Topology/JordanCurve/Basic.lean.
The circle half is TauCeti/Topology/Circle/Arc.lean: a nonempty closed preconnected proper subset
of the circle is a closed arc Circle.exp '' Icc a b with b - a < 2 * π
(TauCeti.exists_eq_circleExp_image_Icc), the two degenerate cases a = b and the empty set being
the point and the empty set, and its complement is the open arc Circle.exp '' Ioo b (a + 2 * π)
(TauCeti.compl_circleExp_image_Icc), path connected as the continuous image of an interval. So a
proper subcontinuum S of the curve is the image of such a closed arc of angles under the
parametrization, and C \ S the image of the complementary open arc.
Nowhere density is the same computation once more. If a < b then the midpoint (a + b) / 2 names
a point of S whose angle lies outside Icc b (a + 2 * π), so it lies outside the image of that
compact interval of angles, which is closed and contains the whole of C \ S; hence that point of
S is not adherent to C \ S, and S is not nowhere dense. Contrapositively, a nowhere dense
compact connected subset is a subsingleton: it is empty, or it has a = b and is a point.
Why this is a layer-L5 prerequisite #
The target is layer L5 of the conformal-mapping roadmap
(TauCetiRoadmap/ConformalMapping/README.md), Carathéodory's boundary correspondence for a Jordan
domain. ConformalMapping/STATUS.md counts the Jordan-curve side of that layer as its
infrastructure, listing Jordan curves with "the arc theory the boundary work needs: two points cut
it into two arcs, and two nearby points cut off a small one", and, of the topological facts about
Jordan curves that the forward direction classically leans on, asks under Plane separation for
Jordan curves that how much of them it needs "should be settled first". The classification of the
compact connected subsets of a curve is one such fact, established here with no conformal input, as
TauCeti/Topology/JordanCurve/Separation.lean settles the cutting of a curve at given points and
TauCeti/Topology/JordanCurve/SmallArc.lean the size of the pieces that cutting leaves. Of the
statements below, TauCeti.IsJordanCurve.isPathConnected_sdiff is a strict generalisation of the
Separation.lean statement for a removed point.
The path from here to that target is one step, and it is a reduction. A boundary cluster set of a
conformal map is already known in this repository to be a continuum contained in the image
boundary (Convex.isConnected_clusterSetOn_of_isBounded together with
TauCeti.clusterSetOn_subset_frontier_image), so for a Jordan domain it is a compact connected
subset of a Jordan curve — and until this file nothing said what such a set can be. The results
here say it: a point, an arc, or the whole curve —
TauCeti.subsingleton_or_exists_injective_path_clusterSetOn, in
TauCeti/Analysis/Complex/Conformal/ClusterSet.lean. L5's forward direction is the assertion that
for a Riemann map the first case always holds, so what this file leaves of it on the Jordan-curve
side is exactly the exclusion of the other two.
TauCeti.IsJordanCurve.subsingleton_of_subset_closure_sdiff excludes both at once from a single
condition on the subcontinuum — that it be nowhere dense in the curve — and that is the step of the
L5 argument this file exists for: fed to
TauCeti.exists_continuousOn_closure_eqOn_of_isBounded — the criterion that turns singleton
boundary cluster sets into a continuous extension on the closure of the domain, and the companion of
the diameter form TauCeti.exists_continuousOn_closure_eqOn_of_forall_exists_diam_union_le that
ConformalMapping/STATUS.md names as proved — it gives
TauCeti.exists_continuousOn_closure_eqOn_of_forall_subset_closure_sdiff, a conformal map of
a convex domain onto a bounded Jordan-bounded region none of whose boundary cluster sets has
interior in the boundary curve extends continuously to closure U. That conclusion is the L5
milestone's conclusion; the hypothesis separating them is relative nowhere density of each boundary
cluster set in the curve. That is a condition on the cluster sets, which depend on the map, its
domain and the boundary point, and not one on the curve by itself: what it drops is the analytic
content of the milestone, not the map.
Verifying that hypothesis for a Riemann map is not attempted here, and nothing here shortens or
replaces the route ConformalMapping/STATUS.md sequences next for it: showing that the boundary
piece a small crosscut cuts off is itself small, which the length–area estimate and the crosscut
files are aimed at, proves singletonness directly.
Generality #
The statements are for a subset of an arbitrary topological space, as in
TauCeti/Topology/JordanCurve/Separation.lean; the subcontinuum is asked to be compact rather
than closed, which is what transports along the parametrization without a separation axiom. Only the
two nowhere-density statements TauCeti.IsJordanCurve.exists_notMem_closure_sdiff and
TauCeti.IsJordanCurve.subsingleton_of_subset_closure_sdiff need the ambient space to be Hausdorff,
because they speak of a closure taken in that space. The corollary
TauCeti.IsJordanCurve.interior_eq_empty is for a real normed space of dimension at least two,
where a ball contains a sphere, which is a subcontinuum with more than one point.
Main results #
TauCeti.IsJordanCurve.subsingleton_or_exists_injective_path— a proper subcontinuum of a Jordan curve is a point or an arc: it is either a subsingleton or the range of an injective path.TauCeti.IsJordanCurve.isPathConnected_sdiff— the complement of a proper subcontinuum in the curve is path connected; for a singleton this isTauCeti.IsJordanCurve.isPathConnected_sdiff_singleton.TauCeti.IsJordanCurve.exists_notMem_closure_sdiff— a subcontinuum with more than one point is not nowhere dense: one of its points is not adherent to the rest of the curve.TauCeti.IsJordanCurve.subsingleton_of_subset_closure_sdiff— the contrapositive, and the form the boundary correspondence consumes: a compact connected subset of a Jordan curve every point of which is adherent to the complement is a subsingleton, so a single point once it is nonempty.TauCeti.IsJordanCurve.interior_eq_empty— a Jordan curve in a real normed space of dimension at least two has empty interior.
References #
- Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
- C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).
Subcontinua of a Jordan curve #
Each statement below transports its circle counterpart along the parametrization
TauCeti.jordanParam e, which is a continuous injection with range the curve. The two private
lemmas carry the closed arc and its complement across it once and for all; the theorems then read
off the consequences.
A proper subcontinuum of a Jordan curve is a point or an arc. A compact preconnected subset of a Jordan curve other than the curve itself is either a subsingleton — the empty set or a single point — or the range of an injective path, which is what it means for it to be an arc.
The path is the closed arc of angles produced by TauCeti.exists_eq_circleExp_image_Icc, carried to
the curve; it is injective because Circle.exp is injective on an interval shorter than a full turn
and the parametrization of the curve is injective outright. Its endpoints, γ 0 and γ 1, are the
two endpoints of the arc.
The complement of a proper subcontinuum in a Jordan curve is path connected. Removing a
compact connected piece other than the whole curve leaves an open arc, in particular a nonempty path
connected set. The case of a single point is
TauCeti.IsJordanCurve.isPathConnected_sdiff_singleton.
Nowhere density #
A subcontinuum with more than one point occupies a relatively open piece of the curve, so it is not nowhere dense there. Stated in the contrapositive this is what identifies a nowhere dense subcontinuum as a subsingleton — a single point once it is nonempty, which is how the classification is used — and it is the form the Carathéodory boundary correspondence spends: a boundary cluster set of a conformal map is a continuum on the image boundary, and this is what degenerates it. Both statements are about a closure taken in the ambient space, so that space is asked to be Hausdorff here.
A subcontinuum of a Jordan curve with more than one point is not nowhere dense in it: one of its points is not adherent to the rest of the curve.
The witness is the midpoint of the arc of angles carrying the subcontinuum. The complement of the
subcontinuum in the curve is the open arc of TauCeti.compl_circleExp_image_Icc, whose closure is
contained in the compact — hence closed — image of the corresponding closed arc, and the midpoint
misses that image because Circle.exp is injective on a period. The subcontinuum is not asked to be
proper: for the whole curve the complement is empty and any of its points will do.
A nowhere dense subcontinuum of a Jordan curve is a subsingleton, so a single point when it is nonempty. If every point of a compact preconnected subset of a Jordan curve is adherent to the complement of that subset in the curve, then the subset has at most one point.
This is the contrapositive of TauCeti.IsJordanCurve.exists_notMem_closure_sdiff.
A Jordan curve in a real normed space of dimension at least two has empty interior.