Invariance of domain

Stream: mathlib4

[Jeremy Ravenel]

Hi, I am new here, so sorry if this comment is misplaced. Noticing that invariance of domain is key here, I would like to ask if there is the Jordan-Brouwer separation theorem in Mathlib Just stating it could be a good intermediate for the invariance of domain.

One would also use the theorem about a continuous function defined on a compact
space (a closed disk 𝔻ⁿ) and valued in a Hausdorff space (here ℝⁿ).

[Michael Rothgang]

Welcome! You ask a good question.
Mathlib has the second result already (can't add the link right now as I'm on the phone). The Jordan curve theorem and invariance of domain would both be great to have. The "correct" proof of either requires the homology groups of spheres.
This has been done in Lean 3 (by Sean Brendas Murphy, search for Brouwer's fixed point theorem on zulip). The homological algebra part has been refactored (and greatly improved) since then, so a line by line port to Lean 4 won't work as-is. Getting that work landed would be really great and a most welcome contribution, though.

[Michael Rothgang]

Mathlib knows about singular homology now (for details, search for a zulip thread with singular homology in the title). Proving it satisfies all the Eilenberg-Steenrod axioms would be the next step. You could use the Brouwer formalisation as an outline (writing the adapted proofs yourself).

[Michael Rothgang]

If that's exactly your cup of tea, I'd be happy to help you get started.

[Michael Rothgang]

So, long answer short: in the near term I don't think these questions affect the question in this thread (I'll move it to a new topic in a moment). That said, progress in them would be fantastic and a most welcome addition to mathlib!

[Jeremy Ravenel]

@Michael Rothgang yes that would he good.

Without of Mathlib, algebraic topology has Spanier-Whitehead duality and Alexander duality concerning complements of finite CW-complexes in spheres. I just learned theorem 3.1 here today.

[Jeremy Ravenel]

3.6 there has the main insight: for a set X inside ℝⁿ and its complement, Y, there is a function f : X × Y → Sⁿ sending (x,y) to (x-y)/||x-y|| and it turns out to produce a dual map in reduced homology.

The axioms would be a good project for me I think.

[Jeremy Ravenel]

For a submanifold of Sⁿ of dimension k, the normal disc bundle used in the theory of Thom classes gives a map from M × 𝔻ⁿ to Sⁿ⁻ ᵏ, which is related to the case in which M is Sⁿ⁻¹ and the normal bundle is 𝔻¹. In that theory, the complement of a normal disc bundle is "equivalence relation fodder" for constructing the Thom space, which is homotopic to the pair (Sⁿ, Sⁿ - M× 𝔻ⁿ⁻ᵏ).

This also has the elegant consequence that the complement of a manifold immersed in a sphere is the pullback of the special point in the Thom space, a based space (@Michael Rothgang ) by the map φ from Sⁿ into Th(M). Maybe all such complements arise in this way!

[Notification Bot]

8 messages were moved here from #mathlib4 > Fixing the definition of models with corners by Michael Rothgang.