Bordism theory

Stream: mathlib4

[Michael Rothgang]

In the past weeks, I have idly worked on formalising the beginnings of bordism theory --- partially out of curiosity how far mathlib is from being able to e.g. define the unoriented bordism groups.

I got surprisingly far, but a bunch of things are also missing. PRed or close to PRing are the following:

• the empty set as a smooth manifold (already merged)
• computed the boundary of a product manifold (#14802; improved in #14972 under review)
• the interval [x,y] has boundary {x,y}, as a manifold: I just PRed this as #15892, with prerequisites #15890 and #15891
• if M is a manifold without boundary, the product M \times [x,y] has boundary M \times {x,y}
• a future PR could include defining singular n-manifolds
• I also defined a class for closed n-manifolds, but @Sébastien Gouezel convinced me this was not necessary: also fine!

I have also formalised a definition of smooth cobordisms, and stated all the missing pieces for making this rigorous. There are about 40 different sorries remaining; I will not close them all. Interesting next projects that are definitely feasible include

• define the disjoint union of two manifolds (over the same charted space and model)
  I have stated the properties I would like. The underlying topological operation should already be defined... so the hard part is smoothness.

• prove that a product M \times {x, y} is isomorphic to the disjoint union of M with itself

• fleshing out the theory of attaching map, by describing pushout in TopCat (there is a file for pullback, so presumably this just needs to be dualised)
• using this to describe the gluing of smooth manifolds along a common boundary: this requires the collar neighbourhood theorem
• deduce that the bordism relation is transitive

branch#MR-bordism-theory is tracking the current progress. The most cleaned up code can be found in PRs.

Most interesting obstacle. The core of bordism theory is the bordism relation, which entails speaking about the boundary of a manifold as a smooth manifold itself --- so we need a notion of "the boundary of this manifold is a smooth manifold itself". Mathlib's theory of manifolds is quite general, and includes e.g. manifolds with corners --- so I added a new typeclass HasNiceBoundary to encode this. BoundaryData encodes (or similar): working with cobordisms then requires passing a chosen smooth structure on the boundary.
I am not yet certain how workable this is: trying to prove some "easy lemmas" runs into some type theory questions, which could be easy and I don't see it, or indicative of a different design being necessary. The section HasNiceBoundary in Bordisms.lean has the details.

I will not have too much time to think about this going forward --- if you feel like building on this, go ahead!

[Ruben Van de Velde]

(deleted)

[Michael Rothgang]

#15906 defines singular n-manifolds

[Michael Rothgang]

Since the last update, I have also

• added some API about disjoint unions of topological spaces (already merged)
• mostly showed that the disjoint union of charted spaces is a charted space (still in progress)

[Michael Rothgang]

#20619 proves that the disjoint union of two charted spaces is a charted space

[Michael Rothgang]

#20659 proves that the disjoint union of two smooth manifolds is a smooth manifolds, and computes its interior and boundary

[Michael Rothgang]

#20664 (still WIP, right now; depending on the previous PR) shows that Sum.inl, Sum.inr, Sum.elim and Sum.map` between smooth manifolds are smooth

[Michael Rothgang]

#15893 (the boundary of a product) is now ready for review. Should be really quick, it's less than 10 lines.

[Michael Rothgang]

#21066 (remove superfluous non-emptiness hypotheses) is another small PR open for review. It depends on #15893 (but that PR is contained to just a single file).

[Michael Rothgang]

#20664 is now ready for review. (The simpNF linter fails: this is one open question from my side, where reviewer input could be helpful.)

[Michael Rothgang]

#21349 (depending on the previous one) proves diffeomorphisms, proving that the disjoint union is commutative, associative etc.

[Michael Rothgang]

Status update:

• merged: #20664, and a few PRs removing superfluous non-emptiness assumptions from the theory
• #21349 is now ready for review

[Michael Rothgang]

#22070 is awaiting review: just 40 lines, proving Is{Open,Closed}Embedding.sum_elim - i.e. purely topological lemmas, which are just filling API gaps

[Michael Rothgang]

#22082 is another easy pre-requisite: just 8 lines of topology

[Michael Rothgang]

Building on the previous two PRs, #22059 adds a more interesting definition: a notion of "smooth manifolds whose boundary is a nice manifold". For now, this just applies to a boundary without boundary (i.e. manifolds without corners), but relaxing this shouldn't be difficult.

The code is still somewhat WIP, in several ways:

• you should only read the first 360 lines of that file (the rest is old code, which I'd like to review and then delete)
• the definition needs one small tweak (which is noted further below in the file)
• a few sorries remain: mfderiv_prod_map is the most significant one
• I have to wrap up my thoughts about sums of boundary data
• to add all the definitions I'd like, this would require quite some API about 0-dimensional manifolds. This is currently missing (see #5462), but probably not difficult.

So, I'm not asking for review yet, but am posting this to indicate future steps.

[Michael Rothgang]

#15906 is ready for review again, code-wise: I haven't documented all design decisions in detail yet.

[Michael Rothgang]

#22083 and #22084 work towards 0-dimensional manifolds: one is an easy definition, the other extends the module doc-string of that file

[Michael Rothgang]

#22107 is an easy code clean-up and pure code motion.

[Michael Rothgang]

#22105 proves that discrete spaces are 0-manifolds. See this thread for the remaining design question.

[Michael Rothgang]

#15906 is ready for review (and passes CI)

[Michael Rothgang]

In the past weeks, I have also (mostly) defined the unoriented bordism groups and proven that they are abelian groups. (#23138 contains all the details.) Landing that into mathlib will take a while though - for instance, as the definition of manifolds with smooth boundary wants to use "this is a smooth embedding". I've opened a separate branch for that.