-
-
Notifications
You must be signed in to change notification settings - Fork 487
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
Refine category of RealSet #31877
Comments
comment:1
Possibly a good idea to consider: #30832 comment:6. |
New commits:
|
Commit: |
Author: Matthias Koeppe |
comment:4
I personally don't like adding Then a forgetful functor would also make more sense. |
comment:5
A |
comment:6
I think this is good. As Matthias said, they are naturally topological spaces from the subspace topology. The only question I have is why is @mjungmath I don't understand what you mean by forgetful functor. These are parents, and have nothing to do with functors. For example, there is a forgetful functor from |
Reviewer: Travis Scrimshaw |
comment:8
Replying to @tscrim:
OK, I'll make this change. |
Branch pushed to git repo; I updated commit sha1. New commits:
|
comment:10
Replying to @tscrim:
I think the idea would be that after applying the functor to the parent, asking for example for the homset would give a different answer. |
comment:11
Replying to @mkoeppe:
IMO, it is better to pass that category information to the homset construction (which you can do) if you want to consider morphisms in a weaker category. This way you have less proliferation of "equal" parents and dealing with elements that maybe shouldn't have the additional structure. In this example, should you be able to add two integers that are in the |
comment:12
Thanks for the change. |
comment:13
Thanks! |
comment:14
Replying to @tscrim:
Just because it comes with a natural topology doesn't mean it is the topology the user wants. If you argument like that, every set must be seen in the category of topological spaces, because every set is endowed with a topology.
Then I don't understand why we even have a forgetful functor if it technically just represents the identity functor... |
comment:15
But I agree, for structures like rings, groups etc. this approach makes total sense. Though, I still don't understand why But for manifolds, things are slightly different. It would be good to have a functor that forgets about the topological structure, for example to impose another one. Like I said, I don't like the idea of enforcing a preferred topology on a set if we see it just as set (what we clearly do with |
comment:16
Replying to @mjungmath:
In #31881 ( |
comment:17
Replying to @mkoeppe:
Good point!
+1 |
comment:18
Just because it acts as the identity on parents, doesn't mean it is the identity functor. Be very careful with confusing abstract and concrete mathematics. If I said By being in the category of topological spaces, you are stating there is a preferred topology. This is akin to the For the manifold code, while it is dynamic, each manifold is not meant to be treated as something that can change. So if you go from differentiable to topological, you either are actually constructing a different object because the maximal atlas is different or it has the same maximal atlas and you still require the maps to be differentiable. We just may not have provided enough information yet to see that difference. |
Dependencies: #31880 |
Branch pushed to git repo; I updated commit sha1 and set ticket back to needs_review. New commits:
|
comment:21
Merged to resolve merge conflict |
Changed branch from u/mkoeppe/refine_category_of_realset to |
we should put it in a suitable subcategory of
TopologicalSpaces
.Depends on #31880
CC: @mjungmath @egourgoulhon @tscrim
Component: categories
Author: Matthias Koeppe
Branch/Commit:
5b0f85d
Reviewer: Travis Scrimshaw
Issue created by migration from https://trac.sagemath.org/ticket/31877
The text was updated successfully, but these errors were encountered: