Meaning of "proper" for topological spaces

Stream: mathlib4

[John Pardon]

I was happy to see the results of the recent LFTCM2024 project on proper actions and basic properties of proper maps. It may be too late at this point, but I thought I'd share some thoughts I had regarding terminology a few years ago. In algebraic geometry, the standard meaning of "proper" is "universally closed and separated". I was for some time unhappy with this (why should these two conditions go together?) and asked a(n in retrospect very badly worded) mathoverflow question about it https://mathoverflow.net/questions/330738/which-definition-of-proper-is-better

Eventually I came to agree with Dustin Clausen's answer that "universally closed and separated" is a useful notion which should have its own name (and why not call this "proper"? that's what it's called in algebraic geometry, and there is no need to have two words "proper" and "universally closed" for the same thing). His reason was based on sheaf cohomology (I won't repeat it here), but there are certainly others. The condition "universally closed and separated" becomes much more natural if one phrases it as "all iterated diagonals are universally closed". For a map of topological spaces, these are equivalent (other than the 0th and the 1st, all higher iterated diagonals are trivial in any 1-category, and the diagonal of a map of topological spaces is an embedding, hence is closed iff it is universally closed). For higher stacks, "all iterated diagonals are universally closed" is the relevant generalization of this notion. In any discussion of stacks, this is what "proper" would mean, which is incompatible with taking "proper" as a synonym of "universally closed" for topological spaces.

[Johan Commelin]

That's a great way of looking at it! Thanks for sharing this

[Anatole Dedecker]

I’m a bit reluctant to switch to universallyClosed in topology (even though it’s equivalent) because I really don’t think about it like this most of the time, but it’s never too late to do a rename if we want. That said, would it be fine to have a separate definition for algebraic geometry, in the same way that we also have docs#AlgebraicGeometry.UniversallyClosed ?

[Patrick Massot]

Hi John, welcome! I’m very happy to see you here. I’ve always thought that your programming skills and mathematical style should bring you to formalized mathematics at some point.

[Patrick Massot]

About your question, I think it’s fine to rename. Beginners will be confused whatever we do because they will expect proper to mean that inverse images of compact sets are compact. So in any case we need good documentation and lemmas relating different definition is specific contexts (such as metric spaces or locally compact spaces). And people will need to be at least vaguely aware that this notion is subtle in general, but that they are one rewrite away from familiar grounds in cases they care about. Even better, people will come here and say: “I have an assumption h : IsProper f, and a compact set K, how do I get IsCompact (preimage f K)?” and the answer will be the same whatever the definition, assuming type class assumptions say we are in an elementary situation. Most people would already not recognize the definition of IsCompact…

[Antoine Chambert-Loir]

I would find reasonable that proper maps are called compact. And if you put hausdorff in your definition of compact, it's even more reasonable to require separated for proper maps. Bizarrely enough, the algebraic geometers of the 60s had the inconsistency of using proper = universally closed plus separated in algebraic geometry, where the hausdorff condition does not hold for the Zariski topology, and universally closed in general topology, where compact sets are requires to be hausdorff.

[Antoine Chambert-Loir]

(In any case, the topological space of the product of two schemes is not the product of their associated topological spaces, so there's no actual mathematical inconsistency, it's just a “bizarrerie”.)

[John Pardon]

I guess the main reason for declaring "proper" := "universally closed + separated" (or, better, all iterated diagonals are universally closed) is simply because the latter is a useful concept which needs a name (the standard name being "proper"), while "universally closed" on its own already has a name. I have a number of complaints about terminology in algebraic geometry (chief among them being "closed immersion") but this looks like one they got right.