Orientation double cover of a manifold with boundary

Stream: new members

[Collin McClellan]

Hello! I come from the land of portals. I have been teaching myself topology and working on a proving the central theorem of portal science: surface independence. Here is my work. As you can see, it is nowhere near formal enough for a lean proof yet, but i hope to get there soon. One important part of my construction is that I am "cutting" a topological manifold in a way that seems to be different from the standard approach: i remove the submanifold and replace it with the orientation double cover as new "edges". Also, i have never seen a definition of odc that works with a manifold with boundary, but i have heard that its not a big issue. Dealing with boundary is important for the case of a portal going through itself. I could not find anything about odc in the lean library. Has anyone worked on that yet?

[Scott Carnahan]

I don't have an answer to your question, but I would suggest replacing "topological manifold" with "smooth manifold" so that working with orientations is easier.