-
Notifications
You must be signed in to change notification settings - Fork 47
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Curry is continuous #926
Curry is continuous #926
Conversation
There are a few definitions that should make their way to the documentation header. |
Do you mind if I rebase and push-force (not sure I can)? |
Yeah of course, I think you should be able to. |
80f33f8
to
bc9b5c1
Compare
Thanks, I'll take a look tonight |
working through uncurry compact-open topology working working through uncurry
better conditions working through uncurry all the currying lemmas
- format doc
Thanks for tidying this all up. I noticed that |
Oh, and a bit of theory I realized after coming back to this:
|
* curry/uncurry of continuous functions * compact-open topology working * removing regular in favor of regular_space --------- Co-authored-by: Reynald Affeldt <[email protected]>
* curry/uncurry of continuous functions * compact-open topology working * removing regular in favor of regular_space --------- Co-authored-by: Reynald Affeldt <[email protected]>
* curry/uncurry of continuous functions * compact-open topology working * removing regular in favor of regular_space --------- Co-authored-by: Reynald Affeldt <[email protected]>
* curry/uncurry of continuous functions * compact-open topology working * removing regular in favor of regular_space --------- Co-authored-by: Reynald Affeldt <[email protected]>
Motivation for this change
Machinery for more function space topologies, and proofs that
curry
anduncurry
are continuous (E.G. curry is a homeomorphism fromU x V -> W
toU -> V -> W
in the right spaces.For more bit more on the why, this is a piece of prep work for homotopy theory. One can define fundamental group of a (path-connected) space
V
asthe connected components of {compact-open, S1 -> V}
. When we're proving things are homotopies, it's far easier to work inU x [0,1] -> V
. But for certain bits of theory, it's much nicer to work in[0,1] -> (U -> V)
instead. E.G. "is homotopic" inherits "is an equivalence relation" from path components. This PR will let us easily move between them with curry/uncurry as we please.When
V
is a uniform space, the compact-open topology and the "family compact" topology agree. But we very rarely need the uniform assumption onV
, so we do the more general work here. We also will need bothS1
and[0,1]
, so we proof these results for any locally-compact, uniform space. The only meaningful issue is thatlocally compact
is slightly too strong. Long story short, the categoryTop
is not cartesian closed, and locally-compact fixes this, but excludes some exotic CW-complexes. A more general form of this works for what's called "compactly generated". That generalization is out of scope for now. My long-term goal is to prove stuff about winding numbers in low-dimensional spaces. Everything will be locally compact for a long time.The HB port should probably do two things
Things done/to do
CHANGELOG_UNRELEASED.md
Compatibility with MathComp 2.0
TODO: HB port
to make sure someone ports this PR tothe
hierarchy-builder
branch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.