Add the category of uniform spaces - #312
Merged
Merged
Conversation
ScriptRaccoon
force-pushed
the
uniform-spaces
branch
6 times, most recently
from
August 1, 2026 07:49
74d0783 to
40d2677
Compare
ScriptRaccoon
force-pushed
the
uniform-spaces
branch
from
August 1, 2026 10:55
40d2677 to
1fb8bc9
Compare
ScriptRaccoon
marked this pull request as ready for review
August 1, 2026 10:55
ScriptRaccoon
force-pushed
the
uniform-spaces
branch
from
August 1, 2026 11:00
1fb8bc9 to
31768b6
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds the category of uniform spaces and uniformly continuous maps. Its properties have also been decided, with two exceptions (see below).
It turns out that there are many similarities with Top, but also some notable differences:
Here, uniform spaces are not assumed to be separated. Later, we should add the category SepUnif of separated uniform spaces as well. (Unfortunately, many authors build separatedness into their definition of a uniform space, which causes unnecessary confusion.)
Undecided properties
Two properties have not yet been decided for Unif, namely regularity and coregularity. I believe that the answers are the same as for Top, namely that the category is coregular but not regular. Gemini has also provided proofs of these claims, but I have not yet had a chance to digest them and would like to merge this PR first. The proofs can be added in later PRs.