PR !4#15906: feat: define singular `n`-manifolds

Stream: triage

[Random Issue Bot]

Today I chose PR 15906 for discussion!

feat: define singular n-manifolds
Created by @None (@grunweg) on 2024-08-17
Labels: awaiting-author, t-differential-geometry

Is this PR still relevant? Any recent updates? Anyone making progress?

[Michael Rothgang]

Still relevant; I was working on it today. My understanding is that this is waiting on some combination of

• me updating to recent master and fixing small nits
• two design decisions: should they be modelled over R^n or any normed space? (I have a new proposal for this, which I'll add soon). And which regularity should be required (I'm fine with allowing any C^n; it doesn't hurt and is not wrong)
• the reviewer understanding the mathematical background
• me updating the whole bordism theory branch to this design (to prove it works). I'm working on that right now.