Boundary injectivity via inverse cluster sets

If IsPreconnectedApproachAt (from TauCeti/Topology/ClusterSet.lean) holds at every boundary point of an open image, the cluster-set continuum theorem makes each boundary fibre of the extension preconnected. The topological core (clusterSetOn_invFunOn_eq_boundary_fiber, isPreconnected_boundary_fiber_of_isPreconnected_image_approach) assumes only IsOpen (f '' U) and continuity of the inverse; the conformal specialization (injOn_closedBall_of_isPreconnected_image_approach) derives these from injective differentiability.

Adapted from D. Cureton, sphere-six-complex, SphereSixComplex/Periods/Uniformization/InverseBoundaryCluster.lean at 895c0a0 (Apache-2.0); cusp-chart material omitted.

Main results

• TauCeti.clusterSetOn_invFunOn_eq_boundary_fiber — boundary fibre = cluster set of the inverse.
• TauCeti.isPreconnected_boundary_fiber_of_isPreconnected_image_approach — connected approach regions ⇒ preconnected boundary fibres.
• TauCeti.injOn_closedBall_of_isPreconnected_image_approach — end-to-end reduction to IsPreconnectedApproachAt.

References

• D. Cureton, sphere-six-complex, SphereSixComplex/Periods/Uniformization/InverseBoundaryCluster.lean at 895c0a0, github.com/deancureton/sphere-six-complex.
• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.

Cluster-set identification and fibre theorems

theorem TauCeti.clusterSetOn_invFunOn_eq_boundary_fiber {U : Set ℂ} {f F : ℂ → ℂ} {a : ℂ} (hUo : IsOpen U) (hfo : IsOpen (f '' U)) (hfi : Set.InjOn f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (ha : a ∈ frontier (f '' U)) : clusterSetOn (Function.invFunOn f U) (f '' U) a = {z : ℂ | z ∈ frontier U ∧ F z = a}

The fibre of a continuous extension over an image-boundary point is the cluster set of the inverse map at that point.

theorem TauCeti.isPreconnected_boundary_fiber_of_isPreconnected_image_approach {U : Set ℂ} {f F : ℂ → ℂ} {a : ℂ} (hUo : IsOpen U) (hUb : Bornology.IsBounded U) (hfo : IsOpen (f '' U)) (hfi : Set.InjOn f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hgc : ContinuousOn (Function.invFunOn f U) (f '' U)) (ha : a ∈ frontier (f '' U)) (hloc : IsPreconnectedApproachAt (f '' U) a) : IsPreconnected {z : ↑(frontier U) | F ↑z = a}

If the image domain is locally preconnected from within at a boundary point, the fibre of a continuous extension over that point is preconnected.

theorem TauCeti.isPreconnected_frontier_fiber_of_image_approach {U : Set ℂ} {f F : ℂ → ℂ} (hUo : IsOpen U) (hUb : Bornology.IsBounded U) (hfo : IsOpen (f '' U)) (hfi : Set.InjOn f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hgc : ContinuousOn (Function.invFunOn f U) (f '' U)) (hboundary : F '' frontier U ⊆ frontier (f '' U)) (hloc : ∀ a ∈ frontier (f '' U), IsPreconnectedApproachAt (f '' U) a) (a : ℂ) : IsPreconnected {z : ↑(frontier U) | F ↑z = a}

A local connected-approach basis at every image-boundary point makes every fibre of the boundary restriction preconnected.

theorem TauCeti.injOn_closedBall_of_isPreconnected_image_approach {f F : ℂ → ℂ} {c : ℂ} {r : ℝ} (hr : 0 < r) (hfd : DifferentiableOn ℂ f (Metric.ball c r)) (hfi : Set.InjOn f (Metric.ball c r)) (hFc : ContinuousOn F (Metric.closedBall c r)) (hFf : Set.EqOn F f (Metric.ball c r)) (hloc : ∀ a ∈ frontier (f '' Metric.ball c r), IsPreconnectedApproachAt (f '' Metric.ball c r) a) : Set.InjOn F (Metric.closedBall c r)

The preceding inverse-cluster reduction, specialized to a disc and fed to Tau Ceti's monotone-extension theorem.