Crosscuts of planar domains

A crosscut of a plane domain U is a simple path whose two endpoints lie on the frontier of U and whose open interior lies in U. Crosscuts are the basic geometric objects used to define prime ends: a prime end is represented by a nested null chain of crosscuts, with two chains identified when they eventually select the same side of each other.

This file introduces the crosscut predicate at the level of paths, proves the elementary API that later prime-end constructions need, and supplies its fundamental nondegenerate examples: chords between distinct points of the boundary circle are crosscuts of an open disc.

The definition uses the open unit interval in the path parameter. This excludes the endpoints from the part required to lie in U, while injectivity prevents a boundary endpoint from being visited again in the interior. For an open U, it follows that the path meets frontier U exactly at its two endpoints.

Crosscuts are unoriented objects geometrically. Accordingly, reversing a path preserves the predicate. The oriented path is nevertheless retained: a prime-end chain will use the order only to choose and compare the components of U cut off by its crosscuts.

Main declarations

• Path.IsCrosscut — a simple path with endpoints on frontier U and interior in U.
• Path.IsCrosscut.range_subset_closure — a crosscut lies in the domain's closure.
• Path.IsCrosscut.range_inter_frontier — it meets the frontier exactly at its endpoints.
• Path.isCrosscut_symm — crosscuts are invariant under reversing orientation.
• Path.IsCrosscut.map_homeomorph — ambient homeomorphisms carry crosscuts to crosscuts.
• Path.isCrosscut_segment_ball — every nondegenerate chord of a disc is a crosscut.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Chapter 2.
• C. Carathéodory, Über die Begrenzung einfach zusammenhängender Gebiete, Math. Ann. 73 (1913).

def Path.IsCrosscut {x y : ℂ} (γ : Path x y) (U : Set ℂ) : Prop

A path is a crosscut of U when it is injective, both endpoints lie on frontier U, and every non-endpoint parameter is mapped into U.

No openness or connectedness hypothesis is built into the predicate. Those are properties of the ambient domain in applications, while retaining the bare predicate makes it usable for relative domains and lets the elementary orientation API avoid irrelevant assumptions.

Equations

• γ.IsCrosscut U = (Function.Injective ⇑γ ∧ x ∈ frontier U ∧ y ∈ frontier U ∧ Set.MapsTo (⇑γ) (Set.Ioo 0 1) U)

theorem Path.isCrosscut_def {x y : ℂ} {γ : Path x y} {U : Set ℂ} : γ.IsCrosscut U ↔ Function.Injective ⇑γ ∧ x ∈ frontier U ∧ y ∈ frontier U ∧ Set.MapsTo (⇑γ) (Set.Ioo 0 1) U

The defining characterization of a crosscut.

theorem Path.IsCrosscut.injective {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : Function.Injective ⇑γ

A crosscut has an injective parametrization.

theorem Path.IsCrosscut.source_mem_frontier {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : x ∈ frontier U

The source of a crosscut lies on the frontier of its domain.

theorem Path.IsCrosscut.target_mem_frontier {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : y ∈ frontier U

The target of a crosscut lies on the frontier of its domain.

theorem Path.IsCrosscut.mapsTo_interior {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : Set.MapsTo (⇑γ) (Set.Ioo 0 1) U

The open interior of a crosscut lies in its domain.

theorem Path.IsCrosscut.source_ne_target {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : x ≠ y

The two endpoints of a crosscut are distinct.

theorem Path.IsCrosscut.range_subset_closure {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : Set.range ⇑γ ⊆ closure U

Every value of a crosscut lies in the closure of its domain.

theorem Path.IsCrosscut.range_inter_frontier {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) (hU : IsOpen U) : Set.range ⇑γ ∩ frontier U = {x, y}

A crosscut of an open set meets its frontier exactly at its two endpoints.

theorem Path.IsCrosscut.symm {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) : γ.symm.IsCrosscut U

Reversing an oriented crosscut gives a crosscut with the opposite orientation.

@[simp]

theorem Path.isCrosscut_symm {x y : ℂ} {γ : Path x y} {U : Set ℂ} : γ.symm.IsCrosscut U ↔ γ.IsCrosscut U

A path is a crosscut exactly when its reversal is a crosscut.

theorem Path.IsCrosscut.map_homeomorph {x y : ℂ} {γ : Path x y} {U : Set ℂ} (hγ : γ.IsCrosscut U) (e : ℂ ≃ₜ ℂ) : (γ.map ⋯).IsCrosscut (⇑e '' U)

An ambient homeomorphism carries a crosscut to a crosscut of the image domain.

theorem Path.isCrosscut_segment_ball {c x y : ℂ} {r : ℝ} (hx : x ∈ Metric.sphere c r) (hy : y ∈ Metric.sphere c r) (hxy : x ≠ y) : (Path.segment x y).IsCrosscut (Metric.ball c r)

A nondegenerate chord of a disc is a crosscut. If x and y are distinct points of sphere c r, then the straight path from x to y is injective, its endpoints lie on the frontier of ball c r, and strict convexity puts every interior point of the chord in the open disc. No positivity hypothesis on r is needed: the sphere of radius 0 is a single point, so two distinct points on it force r ≠ 0.