[Merged by Bors] - feat: separated and locally injective maps #7911
Conversation
alreadydone
added
awaiting-review
|
The proof that coverings are separated is a bit complicated because two facts are missing:
|
|
Is 10 lines long? :) And I'm not sure how to interpret "being separated is local on the base" since I don't assume the base space has a topology in |
|
Currently the proof is very straightforward from the definition, which is the existence of local trivializations Maybe with another definition of covering maps Bourbaki's proof would be easier, but it certainly doesn't look like the case here ... |
|
I'm going to merge this as is. When there is more API of the kind that ACL is talking about, then we can consider golfing the proof. bors merge |
github-actions
bot
added
ready-to-merge
A function from a topological space `X` to a type `Y` is a separated map if any two distinct points in `X` with the same image in `Y` can be separated by open neighborhoods. A constant function is a separated map if and only if `X` is a `T2Space`. A function from a topological space `X` is locally injective if every point of `X` has a neighborhood on which `f` is injective. A constant function is locally injective if and only if `X` is discrete. Given `f : X → Y` one can form the pullback $X \times_Y X$; the diagonal map $\Delta: X \to X \times_Y X$ is always an embedding. It is a closed embedding iff `f` is a separated map, iff the equal locus of any two continuous maps equalized by `f` is closed. It is an open embedding iff `f` is locally injective, iff any such equal locus is open. Therefore, if `f` is a locally injective separated map (e.g. a covering map), the equal locus of two continuous maps equalized by `f` is clopen, so if the two maps agree on a point, then they agree on the whole connected component. This is crucial to showing the uniqueness of path lifting and the uniqueness and continuity of homotopy lifting for covering spaces. The analogue of separated maps and locally injective maps in algebraic geometry are separated morphisms and unramified morphisms, respectively.
|
Build failed (retrying...): |
A function from a topological space `X` to a type `Y` is a separated map if any two distinct points in `X` with the same image in `Y` can be separated by open neighborhoods. A constant function is a separated map if and only if `X` is a `T2Space`. A function from a topological space `X` is locally injective if every point of `X` has a neighborhood on which `f` is injective. A constant function is locally injective if and only if `X` is discrete. Given `f : X → Y` one can form the pullback $X \times_Y X$; the diagonal map $\Delta: X \to X \times_Y X$ is always an embedding. It is a closed embedding iff `f` is a separated map, iff the equal locus of any two continuous maps equalized by `f` is closed. It is an open embedding iff `f` is locally injective, iff any such equal locus is open. Therefore, if `f` is a locally injective separated map (e.g. a covering map), the equal locus of two continuous maps equalized by `f` is clopen, so if the two maps agree on a point, then they agree on the whole connected component. This is crucial to showing the uniqueness of path lifting and the uniqueness and continuity of homotopy lifting for covering spaces. The analogue of separated maps and locally injective maps in algebraic geometry are separated morphisms and unramified morphisms, respectively.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
A function from a topological space
Xto a typeYis a separated map if any two distinct points inXwith the same image inYcan be separated by open neighborhoods. A constant function is a separated map if and only ifXis aT2Space.A function from a topological space
Xis locally injective if every point ofXhas a neighborhood on whichfis injective. A constant function is locally injective if and only ifXis discrete.Given$X \times_Y X$ ; the diagonal map $\Delta: X \to X \times_Y X$ is always an embedding. It is a closed embedding iff
f : X → Yone can form the pullbackfis a separated map, iff the equal locus of any two continuous maps equalized byfis closed. It is an open embedding ifffis locally injective, iff any such equal locus is open. Therefore, iffis a locally injective separated map (e.g. a covering map), the equal locus of two continuous maps equalized byfis clopen, so if the two maps agree on a point, then they agree on the whole connected component. This is crucial to showing the uniqueness of path lifting and the uniqueness and continuity of homotopy lifting for covering spaces.The analogue of separated maps and locally injective maps in algebraic geometry are separated morphisms and unramified morphisms, respectively.