"Proper" definition of a proper map?
What is the proper definition of a proper map?
Here are a few definitions I've come across:
A continuous map $f: X \to Y$ is proper if preimages of compact subsets are compact.
A continuous map $f: X \to Y$ is proper if it is closed with compact fibres.
Kashiwara and Schapira define a map $f: X \to Y$ to be proper if it is closed and its fibres are compact and relatively Hausdorff (two distinct points in the fibre have disjoint neighbourhoods in $Y$).
Definitions 1. and 2. agree when $X$ is Hausdorff and $Y$ is locally compact Hausdorff. Kashiwara and Schapira state that definition 3. agrees with definition 1. when both $X$ and $Y$ are locally compact (and Hausdorff I assume?).
There are also notions of proper morphisms of schemes and proper geometric morphisms of topoi, though I do not really understand these yet. However, I would assume that they should be attempting to capture the same sort of notion of "properness" as in topological category.
It seems that a proper map in some category should satisfy some property, and I am wondering what that property should be. In other words, what is the correct "abstract" definition of properness? I have a feeling it should have something to do with a proper base change theorem in cohomology.
A continuous map $f:X \to Y$ between topological spaces is proper if it is universally closed, i.e., for all $T \to Y$ the induces map \begin{align} X \times_Y T \to T \end{align} is closed. This definition is equivalent to the one you mentioned when $X,Y$ are locally compact Hausdorff. Here $X \times_Y T$ denotes the fiber product in the category of topological spaces (it is just the subspace of $X \times T$ where the maps to $Y$ agree).
A morphism $f: X \to Y$ between schemes is called proper if it is separated, finite type and universally closed. That means that for all morphisms $T \to Y$ the map \begin{align} X \times_Y T \to T \end{align} is closed. This time, $X \times_Y T$ denotes the fiber product in the category of schemes (or locally ringed spaces).
The connection is as follows: Let $a:X \to \operatorname{Spec} \mathbb{C}$ be a smooth proper variety ($a$ is a proper morphism), then the complex manifold $X^{an}$ is compact. More generally, if $f:X \to Y$ is a proper morphism between smooth proper complex varieties, then the analytification of $f$ is a proper morphism of topological spaces (I don't think the smoothness assumption is at all necessary)
In Stacks project, maps satisfying (1) is called quasi-proper and (2) is called proper. (2) is equivalent to being universally closed (proved in Stacks project).
However, it seems natural (at least to me) to define a proper map to be universally closed and separated. This definition is equivalent to (3) (being relatively Hausdorff is equivalent to being separated) and is an analogue of proper morphisms of schemes. Another reason to adopt this definition is that extremally disconnected spaces are exactly SProp-projective objects in $\mathrm{Top}$, where $SProp$ is the class of all surjective proper maps. (See Stone spaces, Johnstone).