Bundle manifolds?

Stream: mathlib4

[Yury G. Kudryashov]

Did we consider bundling manifolds? What are the pros/cons? I haven't thought about it deeply yet.

[Sébastien Gouëzel]

Our whole hierarchy is unbundled: we have spaces, and typeclasses on them that give additional information. I am afraid that mixing unbundled design (for essentially everything) and bundled (for manifolds) would be a recipe for disaster. For instance, a vector space can be seen as a manifold, but if you need a bundling step for this interpretation it would make everything much more complicated.

[Adam Topaz]

I guess bundling could be done in practice in the same way as it is currently done for any other concept that is based on typeclasses, namely via category theory. You could construct the category of manifolds (do we have this btw?), the category of manifolds-with-a-vector-space-structure, and the forgetful functor between them, and work in the bundled world that way.

[Michael Rothgang]

What do you want to use bundled manifolds for? To study a category of them, a new definition ManifoldCat seems best (where hopefully, most results would be derived from results about unbundled manifolds).

[Yury G. Kudryashov]

Sometimes, the same pair of topological spaces have more than one natural ChartedSpace structure. E.g., we can't add an instance saying that a topological AddTorsor is a ChartedSpace, because it would conflict with the ChartedSpace X X instance for topological vector spaces.

[Yury G. Kudryashov]

Of course, bundling charted spaces means that we no longer can treat an unbundled type as a manifold without an explicit mapping.

[Ben Eltschig]

Michael Rothgang said:

What do you want to use bundled manifolds for? To study a category of them, a new definition ManifoldCat seems best (where hopefully, most results would be derived from results about unbundled manifolds).

I was actually thinking about defining the categories of finite-dimensional manifolds and Banach manifolds recently, because there are some results about them I would like to formalise. I'm unsure what the best way to systematically define categories like that would be though: there are a lot of different categories of manifolds, depending on which restrictions like Hausdorffness, paracompactness, boundarylessness, finite-dimensionality etc. you want to impose. Do we want one category with almost no restrictions, that all the other categories would be full subcategories of? That would probably be closest to a type of bundled manifolds, but I'm unsure how relevant it would be in practice

[Ben Eltschig]

One thing I'm relatively sure though is that categories of manifolds should allow each manifold to carry its own model space as data, instead of requiring all manifolds to be modelled on the same space - we want e.g. a category of finite-dimensional manifolds, not a category of manifolds modelled on some specific finite-dimensional space like $\mathbb R^3$. So if you want a type of bundled manifolds over a fixed model space, that would not be it

[Ben Eltschig]

Yury G. Kudryashov said:

Sometimes, the same pair of topological spaces have more than one natural ChartedSpace structure. E.g., we can't add an instance saying that a topological AddTorsor is a ChartedSpace, because it would conflict with the ChartedSpace X X instance for topological vector spaces.

Could the solution here maybe be to instead replace the charted space instance on vector spaces with one on torsors? Or are the two actually different in the case of vector spaces?

[Yury G. Kudryashov]

We have an instance [TopologicalSpace X] : ChartedSpace X X.

[Ben Eltschig]

Oh, I see. That seems harder to resolve indeed