What will the Jordan Curve Theorem look like in mathlib?

Stream: mathlib4

[A. M. Berns]

Building on some recent discussion related to this, I'd like to ask the community what we think the statement of the Jordan Curve Theorem will be once it is formalized into mathlib. I'm not sure whether anyone is actually actively working on formalizing the JCT itself, but I think having an agreed-upon statement even without a proof would unlock a lot. For example, I am working on defining the interiors of polygons, but to do this right requires the JCT. So what will the JCT look like? Will the ambient space be only EuclideanSpace ℝ (Fin 2), any manifold homeomorphic to that, or something else? How is the statement itself likely to look?

[Kevin Buzzard]

This is a great question. Smooth Jordan curves show up twice in recent Annals papers, once defined as maps into $\R^2$ and once defined as maps into $\mathbb{C}$. I asked about putting the definition into mathlib a few weeks ago and was told that probably mathlib didn't want a definition.

[Snir Broshi]

cc @Sébastien Gouëzel

[Snir Broshi]

I feel like there's enough discussion for an issue to collect all of it: #35222

[Sébastien Gouëzel]

Here is a version of the Jordan curve theorem as I envision it in Mathlib: let E be a finite dimensional normed real vector space of dimension \ge 2, let f : sphere (0 : E) 1 -> E be a continuous injective map, then E \ range f has two connected components.

[Sébastien Gouëzel]

With specialized versions when the dimension is 2, and the source of f could be any of our versions of the circle

[Junyan Xu]

The statement in #mathlib4 > Jordan curve / Smooth Jordan curve @ 💬 is already pretty close to the established statement in HOL Light (see p.7 in the linked PDF in forwarded message below); I think it's good to generalize it to 2D real normed space. I've also wondered whether we should define winding numbers in 2D real normed space; probably I'll just define it first for Complex then transport by homeomorphisms.
image.png
Junyan Xu said:

This is another nice account of the development of simplicial homology in HOL light: it also covers the Jordan-Schoenflies theorem (a strengthening of Jordan curve theorem that requires complex analysis) and the Jordan-Brouwer separation theorem (higher dimensional generalization).