Dennis Sweeney

Stream: new members

[Dennis Sweeney]

Hello all,

I'm Dennis, and I'm a graduate student studying algebraic topology at the Ohio State University.

I'm currently (with the help of Prof. @Jim Fowler ) trying to formalize in Lean a proof that classifies the (connected, Hausdorff, second-countable) topological 1-manifolds with boundary (Ioo, Icc, Ico, or circle). My work so far is here, but in particular there are some facts about connected sets of reals that might be useful to have in mathlib.

The how to mentioned that I should request write access to add a branch on the main mathlib repo, so I'd like to do that: my github username is sweeneyde.

Thanks!

[Bolton Bailey]

@maintainers

[Michael Rothgang]

I would be excited to see your project hit mathlib! (That result is foundational to some differential topology results, and imho definitely belongs in mathlib.)

[Anatole Dedecker]

@Dennis Sweeney Invitation sent!

[Kevin Buzzard]

Consider it a warm-up for classification of closed surfaces :-)

[Michael Rothgang]

Kevin Buzzard said:

Consider it a warm-up for classification of closed surfaces :-)

That's also on my big list of things I'd like to see - and I would be happy to contribute to at least stating it.

[Kevin Buzzard]

There was a recent discussion here.

[Michael Rothgang]

Recently, I came across this question again: having the classification of 1-manifolds would be very valuable for an easy case of bordism theory (which I'm playing with at the moment). What's the current status of your work? (I saw a PR to mathlib, a while ago, which turned out to be mostly present already, in more abstract form. I'm not sure if/what happened since then.)

[Michael Rothgang]

Perhaps relatedly: mathlib has notions of the interior and boundary of a manifold. (It doesn't have that the boundary is a manifold again, but I'm thinking about that direction right now: mathlib's definition of manifolds is very general, and also allows e.g. corners - so "boundary is a submanifold" is an additional condition and not implies by mathlib's set-up. I'll probably open a separate thread about this soon.)

[Michael Rothgang]

One nice fact to have would be that the boundary of a (non-empty real) interval $[x,y]$ is in fact the set $\{x,y\}$. @Dennis Sweeney Is that something you thought about, or does your intended proof proceed differently?

[Eric Wieser]

@loogle frontier, "Icc"

[loogle]

:search: frontier_Icc

[Yaël Dillies]

I think Michael means "boundary as a manifold"

[Michael Rothgang]

I had seen frontier_Icc, but that's not yet what I need. :-)

[Michael Rothgang]

Continuing at this thread