Can anyone recommend a finitist, constructivist approach to topology? I’m really most interested in discrete geometry, but a geometry that doesn’t try to preserve traditional concepts like curvature, angle, volume etc, but builds them up from scratch from finite graphs. A discrete-first approach, like how Lattice Boltzmann methods are approximated by Navier Stokes rather the way FEM solvers discretize Navier Stokes.
The requirement for finiteness means you are just working with lattices. Topology approached via frame homomorphisms (like in the nlab book) makes this clear.
Thanks! By nlab book you mean the whole nlab project? Also, can you help me understand the connection to lattices? Do they model intersection and union of open sets? Why is finiteness needed for lattices to be appropriate?
I meant [1] they use frames [2] to explain what a topology is but in a finite setting the frame becomes a lattice because you only have finite meets and joins.
For topology, there are two main constructive approaches.
The first, better-developed one, can be found in the theory of locales. An easy intro is Vickers' Topology via Logic, from which you can level up to Johnstone's Stone Spaces.
This approach is suitable for a background logic which is constructive, but accepts the powerset axiom. If you want to restrict yourself to not just be constructive, but also predicative, then the thing to look at is Sambin's formal topology, which he surveys in his 2001 paper Some Points in Formal Topology. (https://www.math.unipd.it/~sambin/txt/SP.pdf)
6 comments
[ 3.1 ms ] story [ 23.8 ms ] threadDisclaimer: not a mathematician (yet)
[1]: https://ncatlab.org/nlab/show/Introduction+to+Topology [2]: https://ncatlab.org/nlab/show/frame
For topology, there are two main constructive approaches.
The first, better-developed one, can be found in the theory of locales. An easy intro is Vickers' Topology via Logic, from which you can level up to Johnstone's Stone Spaces.
This approach is suitable for a background logic which is constructive, but accepts the powerset axiom. If you want to restrict yourself to not just be constructive, but also predicative, then the thing to look at is Sambin's formal topology, which he surveys in his 2001 paper Some Points in Formal Topology. (https://www.math.unipd.it/~sambin/txt/SP.pdf)
https://staff.math.su.se/anders.mortberg/papers/cubicalsynth...