Monotone maps from a Jordan curve

A continuous map from a Jordan curve is called monotone when each of its point fibres is connected. This file records the rigidity consequence needed by the Carathéodory boundary correspondence: a monotone map whose fibres have empty interior is injective.

The argument is intrinsic to the curve. A point fibre is compact by continuity and compactness of the Jordan curve, and it is preconnected by monotonicity. If it had two points, the classification of subcontinua of a Jordan curve in TauCeti/Topology/JordanCurve/Subcontinuum.lean would force it to contain a relative open arc. Equivalently, the nowhere-dense criterion TauCeti.IsJordanCurve.subsingleton_of_subset_closure_sdiff makes every fibre a subsingleton.

The theorem is phrased for a map whose domain is the subtype C. Thus its fibres and their interiors are taken in the topology of the curve itself, which is the natural form for boundary maps and avoids an ambient-space side condition.

Main result

• TauCeti.IsJordanCurve.injective_of_isPreconnected_fiber_of_interior_fiber_eq_empty — a continuous map from a Jordan curve with preconnected, interiorless point fibres is injective.
• TauCeti.IsJordanCurve.injective_iff_isPreconnected_fiber_of_interior_fiber_eq_empty — under the same interior condition, monotonicity is equivalent to injectivity.

References

• G. T. Whyburn, Analytic Topology, Ch. VII.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.

theorem TauCeti.IsJordanCurve.injective_of_isPreconnected_fiber_of_interior_fiber_eq_empty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T1Space Y] {C : Set X} {g : ↑C → Y} (hC : IsJordanCurve C) (hg : Continuous g) (hpre : ∀ (y : Y), IsPreconnected {x : ↑C | g x = y}) (hinterior : ∀ (y : Y), interior {x : ↑C | g x = y} = ∅) : Function.Injective g

A monotone map from a Jordan curve with interiorless fibres is injective. Let C be a Jordan curve and g : C → Y a continuous map to a T₁ space. If every point fibre of g is preconnected and has empty interior in C, then g is injective.

Continuity makes each fibre closed, hence compact because C is compact. Empty interior says its complement is dense. The fibre is therefore a nowhere-dense subcontinuum of the Jordan curve, so TauCeti.IsJordanCurve.subsingleton_of_subset_closure_sdiff makes it a subsingleton.

theorem TauCeti.IsJordanCurve.injective_iff_isPreconnected_fiber_of_interior_fiber_eq_empty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T1Space Y] {C : Set X} {g : ↑C → Y} (hC : IsJordanCurve C) (hg : Continuous g) (hinterior : ∀ (y : Y), interior {x : ↑C | g x = y} = ∅) : Function.Injective g ↔ ∀ (y : Y), IsPreconnected {x : ↑C | g x = y}

For an interiorless-fibre map from a Jordan curve, monotonicity is equivalent to injectivity. The forward implication is TauCeti.IsJordanCurve.injective_of_isPreconnected_fiber_of_interior_fiber_eq_empty. Conversely, an injective map has empty or singleton point fibres, hence preconnected fibres; this direction needs neither continuity nor the Jordan-curve hypothesis.