feat: define singular n-manifolds

[grunweg]

These are used to define bordism groups: the n-bordism group of a topological space X is the space of cobordism classes of all singular n-manifolds on X.

---

This PR can be seen in context in this branch (old version; more updated version (in progress) is here.

#22059 (still in progress) defines manifolds with smooth boundary; very soon, I'll file a PR depending on this and #22059 for the definition of bordism groups.

[github-actions]

PR summary 546982219f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.Bordisms (new file)	1923

---

Declarations diff

+ SingularNManifold.{u}
+ comap
+ comap_f
+ empty
+ instIsManifoldModelSpace
+ instance {s : SingularNManifold X k I} : BoundarylessManifold I s.M := s.boundaryless
+ instance {s : SingularNManifold X k I} : ChartedSpace H s.M := s.chartedSpace
+ instance {s : SingularNManifold X k I} : CompactSpace s.M := s.compactSpace
+ instance {s : SingularNManifold X k I} : IsManifold I k s.M := s.isManifold
+ instance {s : SingularNManifold X k I} : TopologicalSpace s.M := s.topSpaceM
+ map
+ map_comp
+ map_f
+ prod
+ refl
+ sum
+ toPUnit
- intIsManifoldModelSpace

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Note to self: merge my improvements to the bordism theory branch here, once the dependent PR has landed.
Update: done now, and cleaned up this PR.

[alreadydone]

I'd suggest that you use EuclideanSpace ℝ n and get rid of E and H.

[grunweg]

This makes speaking about products more difficult: when talking about products of bordism classes and the (un)oriented bordism ring, that would be needed. Why would you use euclidean space instead?

[grunweg]

I have changed my mind again, to parametrising the definition over E and H instead: this allows disjoint unions (which require the same model space) and products (take ModelProd), but does not close the door to using EuclideanSpace R n in applications.

[sgouezel]

Can you sketch a little bit more the maths behind this, which I don't know? (For me, a cobordism between two manifolds M and N is a manifold one dimension higher with two boundary components which are diffeomorphic to M and N respectively, but I don't see how your singular manifolds fit into this picture). Either in the file-level docstring, or in the PR, as you prefer.

I think it would help me a lot to see a theorem which is proved with this formalism (the proof of the pudding is in the eating). Do you have a working branch with a specific theorem you could point me to, so that I get a better grasp of where you want to go? (Ideally you could even open a PR with a work in progress branch, for easier discussion there)

[YaelDillies]

Do you have a working branch with a specific theorem you could point me to, so that I get a better grasp of where you want to go?

The PR description links to master...MR-bordism-theory

[grunweg]

Thanks for the review! I agree that not everything is self-explanatory; let me expand on the background.

About bordisms: the first time I heard about cobordisms, it was the definition you mentioned. The general definition involves an additional map: two singular n-manifolds (M,f:M\to X) and (N,g:N\to X) are cobordant if there's a cobordism between them --- which is a compact (n+1)-manifold W together with a map F\to X such that

• the boundary of W is diffeomorphic to the disjoint union of M and N, and
• under this diffeomorphism, the map F restricts to f resp. g.

In particular, if X is a one-point space, one arrives at the definition you give.

References. I learned this from my advisor's course (see these notes, week 14). I'm just formalising parts of the first page... as formalisation takes more time and space so far.
Dan Freed's lecture notes (https://web.ma.utexas.edu/users/dafr/bordism.pdf) are also supposed to be pretty good.
The manifold atlas page http://www.map.mpim-bonn.mpg.de/B-Bordism#Piecewise_linear_and_topological_bordism has much more generality. Mathlib is not ready for that yet, not even close.

Bigger picture for this PR. As Yael mentioned, this branch has my overall work so far, leading up to defining the unoriented bordism groups. At the end, I realised I needed to change the design of singular n-manifolds (to the current one); I haven't gone through and adapted all of that branch yet. When I do, it shouldn't be too hard to prover that the unordered bordism group is a group.
There are a number of sorries, most of which are missing pre-requisites like "the disjoint union of two n-dimensional manifolds is an n-manifold". Doable, should be in mathlib, but someone needs to do it. (And I'm supposed to work on e.g. the Carleson project now.)

[grunweg]

I have just adapted this PR to latest master, and also

• generalised the definition to C^n manifolds: while smooth bordism groups are the most classical ones, and the basis for e.g. the continuous case as well, the definition of singular n-manifolds generalises to the continuous setting, and is also used there.

• thought about the model space question: it would surely be nice if we could just use R^n, but I don't think it's that simple. Medium-term, we'd like to perform two constructions with singular n-manifolds: take the direct sum (to define bordism groups), and take the product (for the bordism ring).
  Taking products means we'll have to take ModelProd as a model space, and using R^n and R^m becomes painful to impossible to use here: we have to do something else. On the other hand, the direct sum construction requires the same model space for now. However, that step is more flexible: if we have an equivalence of the model to a common model, we can translate the charted space structures are still reach our goal.
  This yields the eventual definition I chose: model singular n-manifolds on some space H, but keep a homeomorphism to R^n around (which is used for the direct sum).

• I am not sure about the universes: the checkUnivs linter still complains if I change them as you say.

There are three sorries remaining, but none of them is mathematically problematic (nor interesting).

[grunweg]

Actually, the other sorry is interesting. I'll think about it more and update this PR accordingly.

TODO: this PR was updated, write a comment here explaining my choices. Perhaps after polishing the boundary PR and submitting the definition of bordism groups.

[sgouezel]

Suggested change

	We don't assume `M` to be modelled on `ℝ^n` (nor to be using with the standard model),
	We don't assume `M` to be modelled on `ℝ^n` (nor to be using with the standard model),

I'm not sure I understand the parenthesis here. Could you clarify?

[sgouezel]

Could you expand a little bit the docstring here, to explain what singular n manifolds are: it's not manifolds where you allow some singularities (which is what the name seems to indicate), it's rather a smooth manifold enriched with a continuous map to a topological space X. Also explain that, for X = a point, you just get manifolds in the usual sense. And maybe sketch an example of something that can be done with this formalism but which can not be done using manifolds in the usual sense?

Note that wikipedia, for instance, only defines bordism in the usual sense (where two manifolds are cobordant if they are the boundaries of a one-dimensional higher manifold), so it's a little bit surprising to say that you are doing "the beginnings of bordism" and go directly to a slightly exotic setting. So I think this deserves big warnings, and motivation in the docstring.

[grunweg]

I will expand this doc-string (thanks for providing some hints). However, let me say that your claim about wikipedia is not fully correct: it mentions bordism groups as an extraordinary cohomology theory https://en.wikipedia.org/wiki/Cobordism#Cobordism_as_an_extraordinary_cohomology_theory. There are absolute and relative bordism groups; wikipedia only hints at this fact (and mostly mentions the absolute ones).

[sgouezel]

You're absolutely right! What got me is that I looked for the word "singular" in the wikipedia page and didn't find it. Is the terminology "singular manifold" for a manifold together with a map to X completely standard?

[sgouezel]

I don't see W below

[sgouezel]

I am confused by the design and the comment here. One you fix I, you are fixing the model space, so by definition s and t have the same model space, and there is nothing special to do: just use I also for the disjoint union. On the other hand, it makes me realize that the parameter n is completely useless in all the story, as it is also determined by I (it's the dimension of the target space of I). So why not just remove it completely from the definition of SingularNManifold (and from the whole file)?

[grunweg]

Thanks for the review comments! I responded to some of your comments/addressed the easier ones (which were very helpful). This PR will require some more polish on my parts - leaving as awaiting-author until I've had the time to address them.