Commit 2023-11-03 10:44 83b113a5

feat: separated and locally injective maps (#7911) 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.