Jordan curve / Smooth Jordan curve

Stream: mathlib4

[Kevin Buzzard]

There are two recent papers in the Annals which prove theorems about smooth Jordan curves. Does anyone have an opinion about the generality in which this definition should be in mathlib, if indeed it should be there at all?

A Jordan Curve is typically defined as a subset of $\mathbb{R}^2$ which is homeomorphic to a circle. But should this really be some predicate on subsets of topological spaces? Or is this absurd? I think it's worth remembering that the big fact about Jordan curves is that it splits the plane into two pieces (so who cares about topological spaces) and the big conjecture about Jordan curves is that they all contain the corners of a square (and for this we need some notion of angle and straight line).

For this square/rectangle question people also work with Smooth Jordan Curves, which are the image of a smooth embedding of S^1 into R^2. So here one could make the definition for subsets of a smooth manifold, but again people tend to ask questions about whether they contains corners of rectangles and so again one needs some kind of 2d assumption and the concept of angle/straight line.

Should we just define Jordan curves for $\R^2$, or things isometric to $\R^2$, or in some ridiculous generality? I am not clear about the generality that people care about these things, and then there's also this push in mathlib to have definitions as ridiculously general as we can make them (and in particular that might mean a different level of generality for Jordan curve and smooth Jordan curve).

[Thomas Browning]

Bear in mind that if we defined smooth Jordan curves for arbitrary smooth manifolds, then we would end up with the definition of a smooth knot!

[Johan Commelin]

I think @Sébastien Gouëzel pointed out a while ago, that there are higher-dimensional variants of the Jordan curve theorem, and we should aim for those.

[Johan Commelin]

If I remember correctly: if you have a subset of $\R^{n+1}$ that is homeomorphic to $S^n$, then the complement has 2 connected components.

[Michael Rothgang]

There was previous discussion about this recently: let me try to find it (within the next hour).

[Sébastien Gouëzel]

I don't think we should have a definition of a smooth Jordan curve (whatever that means): it should be enough to just talk about the image of the circle under a C^1 injective map (possibly with non-vanishing derivative depending on what the notion really means, and possibly with a higher smoothness), no need to over-engineer there.

[Michael Rothgang]

It was around here: #maths > Multivariate complex analysis @ 💬

[Joseph Myers]

https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/InscribedSquare.lean has the inscribed square problem. Once we have polygons in mathlib (@Anson Berns expressed an interest in defining polygons in the context of working on Pick's theorem but I haven't yet seen a PR to mathlib with a definition) we should probably add definitions of such things as "is a square" (= is nondegenerate convex regular 4-gon) and "is a rectangle", so that that doesn't need to stay as a definition local to that conjecture, but the way it's expressing Jordan curves seems fairly reasonable; it's using IsEmbedding (you could argue whether you want "embedding" or "injective continuous map" for the definition, but in this context they're equivalent).

[Joseph Myers]

The Jordan-Brouwer separation theorem is an n-dimensional version of the Jordan curve theorem and it would indeed be good to have in mathlib (other variants may be useful as well; in particular it would be good to have Jordan-Schoenflies as a stronger version of the Jordan curve theorem in two dimensions).

[A. M. Berns]

Joseph Myers said:
@Anson Berns expressed an interest in defining polygons in the context of working on Pick's theorem but I haven't yet seen a PR to mathlib with a definition

I have begun working, but I'm not ready to PR yet. My strategy, although perhaps disappointing, is to take the JCT as an axiom. I don't think it's very sensible to talk about area without it, and I hope it will be formalized into Lean at some point, so I think having things like JCT -> Pick's is useful. I've written the axiom version of JCT (for 2-dimensional Euclidean space) as follows:

def IsSimpleClosedCurve (γ : Set (EuclideanSpace ℝ (Fin 2))) : Prop :=
  ∃ f : AddCircle (1 : ℝ) → EuclideanSpace ℝ (Fin 2),
    Continuous f ∧ Function.Injective f ∧ range f = γ
structure JordanDecomposition (γ : Set (EuclideanSpace ℝ (Fin 2))) where
  interior : Set (EuclideanSpace ℝ (Fin 2))
  exterior : Set (EuclideanSpace ℝ (Fin 2))
  partition : γ ∪ interior ∪ exterior = univ
  interior_isConnected : IsConnected interior
  exterior_isConnected : IsConnected exterior
  interior_isOpen : IsOpen interior
  exterior_isOpen : IsOpen exterior
  interior_isBounded : Bornology.IsBounded interior
  exterior_not_bounded : ¬Bornology.IsBounded exterior
  frontier_interior : frontier interior = γ
  frontier_exterior : frontier exterior = γ
noncomputable axiom jordan_curve_theorem {γ : Set (EuclideanSpace ℝ (Fin 2))}
    (hγ : IsSimpleClosedCurve γ) : JordanDecomposition γ

I'm going to use this to define the interior and area of a polygon. I'm very open to hearing feedback on how this can best be amended so that the infrastructure can be most generally useful and will most directly connect to the JCT as it will be proved.

[Joseph Myers]

Small PRs (no more than a few hundred lines, maybe less) are good. A PR that just defines polygons (for points in an arbitrary type) and makes a few very basic definitions (for points in an affine space, or an affine space over the reals when needed) - nothing specifically to do with Pick's theorem - would be good, then people can review the API setup and start making their own contributions for other things they want to use polygons for. Basic definitions include things like "vertices are coplanar", "polygon is convex", "no two consecutive vertices equal", "no three consecutive vertices collinear", "boundary is a simple curve", ... - very basic nondegeneracy properties (that should be separate predicates, not part of the definition of Polygon, because different lemmas may need different subsets of those properties).

[Joseph Myers]

If more than one person is interested in doing things using a given definition or lemma, that's a good reason to start PRing it early. Things that are more specific to Pick's theorem rather than other uses of polygons might sensibly wait until later for PRing to mathlib.

[A. M. Berns]

Fair enough. I'll PR soon. I wasn't really sure what the etiquette around it was. My current definition of Polygons is very minimal, but for area I'm basically only going to be working with SimpleEuclideanPolygons with additional properties.

[A. M. Berns]

I submitted a PR with a definition of Polygons. I posted a separate thread for discussion of it here. I also mention in that thread that I am planning on using a version of the Jordan Curve Theorem as an axiom in working with polygon areas.