Terminology for point-free topology?

[Steven Vickers <s.j.vickers.1@bham.ac.uk>]

I'm wondering if there's any consensus usage to found for "point-free" topology and related terms.

I've posted a detailed discussion on https://arxiv.org/abs/2206.01113, but I can summarize the question more succinctly.

It's not unusual to distinguish between two synonymous pairs:
   point-set/pointwise = ordinary semantics of general topology,
   point-free/pointless = reformed semantics of, e.g., locales or formal topology.

However, that is misleading, as locale theory can be validly done using points. See, e.g., Ng-Vickers on real exp and log, https://lmcs.episciences.org/9879. The trick is to restrict to geometric constructions and to apply them to *generalized* points, to be found in arbitrary Grothendieck toposes and not just Set (or your chosen base S).

Thus there are two distinctions to be made -

1 Ordinary semantics v. reformed
2 Use points v. avoid them

Some terms naturally fall into place.

Point-set = ordinary topology, points taken from a given set.

Pointwise = use points. Point-set is a subclass of pointwise, but strict,  as shown by the above example.

What about pointless and point-free? I'm piloting -

Pointless = avoid points (e.g. construct locale maps concretely as frame homomorphisms). There's some value judgement in my choice there, as very often the pointwise reasoning is simpler and more transparent, so there seems  to be no good reason for arguing pointlessly.

Point-free = reformed topology. I try to think of this as meaning that the points are liberated from their confinement to Set or S.

Does anyone have comments on these, or suggestions for other phrases for the concepts?

Happy New Year!

Steve Vickers.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]