Cobordism hypothesis in 1-dimension.

Stream: maths

[Joseph Tooby-Smith]

I am interested in the possibility of formalizing the proof of the cobordism hypothesis for topological field theories in 1-dimension in lean. Potentially following arXiv:1210.0229.

Do people think this would be possible?
Getting ahead of myself - if there is another interest, maybe it is worth setting up a GitHub repository with this aim in mind.

(Sorry if this is the wrong stream to ask this.)

[Johan Commelin]

Can you list some of the ingredients that would be needed for this?

[Joseph Tooby-Smith]

Symmetric monoidal infinity-categories and functors between them (basically the first few chapters of Lurie's higher topos theory, and higher algebra books). We would also need some properties of oriented 1-dimensional manifolds, maps between them, isotopies between those etc.

[Johan Commelin]

I think symmetric monoidal infty cats might be a pretty tough challenge.

[Michael Rothgang]

AFAICT, mathlib doesn't have the classification of 1-manifolds yet - this would be useful in its own (and fairly doable, I'd think). Differential topology uses this all of the place. I'd be excited to see this; I cannot say yet if I'd have time to join this effort.

[Kevin Buzzard]

Yeah I was going to say that it might be the case that oriented 1-dimensional manifolds was more of a challenge! We have very little about manifolds beyond basic definitions of manifolds and vector bundles incl tangent bundle.