Jordan separation on the Riemann sphere

A Jordan curve J in the Riemann sphere OnePoint ℂ separates it: Jᶜ is not preconnected. This is the Jordan–Brouwer separation theorem for the two-sphere, TauCeti.natCard_zerothHomotopy_sphere_compl_range_eq_two, transported along Mathlib's stereographic homeomorphism onePointEquivSphereOfFinrankEq, in the connected form TauCeti.not_isPreconnected_compl_range_sphere that holds because the sphere is a manifold. Transported the same way, the count itself says that Jᶜ has exactly two path components.

The consequence used for unbounded Jordan domains is an exterior point. If U ⊆ ℂ is open and connected and its frontier, together with the point at infinity, is a Jordan curve of the Riemann sphere, then some point of ℂ lies outside closure U. Otherwise U is dense, its frontier is Uᶜ, and the complement of the curve is the image of the connected set U. Inverting U about such a point turns it into a bounded Jordan domain of the plane.

Main results

• TauCeti.IsJordanCurve.not_isPreconnected_compl_onePoint — a Jordan curve separates the Riemann sphere.
• TauCeti.IsJordanCurve.natCard_zerothHomotopy_compl_eq_two_onePoint — the Jordan curve theorem on the Riemann sphere: the complement of a Jordan curve has exactly two path components.
• TauCeti.exists_notMem_closure_of_isJordanCurve_insert_infty — an open connected set whose frontier, together with the point at infinity, is a Jordan curve of the Riemann sphere has a point outside its closure.

References

• A. Hatcher, Algebraic Topology, Section 2.B, Corollary 2B.2.

theorem TauCeti.IsJordanCurve.not_isPreconnected_compl_onePoint {J : Set (OnePoint ℂ)} (hJ : IsJordanCurve J) : ¬IsPreconnected Jᶜ

The Jordan separation theorem on the Riemann sphere. The complement of a Jordan curve in OnePoint ℂ is not preconnected.

theorem TauCeti.IsJordanCurve.natCard_zerothHomotopy_compl_eq_two_onePoint {J : Set (OnePoint ℂ)} (hJ : IsJordanCurve J) : Nat.card (ZerothHomotopy ↑Jᶜ) = 2

The Jordan curve theorem on the Riemann sphere. The complement of a Jordan curve in OnePoint ℂ has exactly two path components.

theorem TauCeti.exists_notMem_closure_of_isJordanCurve_insert_infty {U : Set ℂ} (hUo : IsOpen U) (hUc : IsPreconnected U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) : ∃ (q : ℂ), q ∉ closure U

An unbounded Jordan domain has an exterior point. If U ⊆ ℂ is open and preconnected and its frontier, together with the point at infinity, is a Jordan curve of the Riemann sphere, then some point of ℂ lies outside the closure of U.