On 09/02/2025 17:45, Waldek Hebisch wrote: > Finite topological spaces are equivalent to partial orders, so > there is connection to logic. But they are quite different than > infinite topological spaces like simplicial complexes.
I hope there is a way to implement a 'geometric realization' function, that is an algorithm to embed a finite topological space in a vector space (which is a Euclidean space, which is a topological space). In the opposite direction I would also like to implement a 'nerve construction'. I would also like to link these to logic/frames as in Steven Vickers book 'Topology via Logic' but at this stage I am just trying to work out what's possible. > Let me present my view here. What does it mean "doing mathematics > in computer"? One aspect is to support notation analogus to used > in literature, allowing creation and manipulation of statements/ > expressions. In particular this means reasonably nice output. > Basicaly this would be "programmable editor", so transformation > could be specified by hand. Are you talking about a graphical editor for Topology/Geometry that would give an equation editor and draw the result in real time? This would be very nice but not the sort of thing that could be written in SPAD? > Nontrivial mathematical statements > may be hard or impossible to decide, so I do _not_ expect > general domain of this sort to be able to say decide mathematical > equality. But hopefully user should be able to specify > transformations and see their effect. Well for finite topology code (as opposed to the existing simplicial complex code in alg_top.spad) I would like the 'equalities' to be Homeomorphism (a cup is the same as a doughnut) and homotopy equivalence (a line is the same as a point). Since these are defined like isomorphism with maps in both directions I would like some way to create, combine and use continuous maps. So I think I would need a domain to represent a continuous map. Presumably as a subset of a product, that is, a set of (input,output) pairs for the points combined with something similar in the reverse direction for the open set preimage. This all seems very messy and unwieldy which is why I like the idea of implementing it as database tables. I know there is a database domain in FriCAS but I think that's just for internal FriCAS metadata? One advantage of having a database is that it makes it easier to implement a pullback which seems to be the fundamental construct where a lot of this structure comes from. So this would be a database search which would only enable the inputs which go to the same place when they go different ways around the square. Perhaps a full database implementation is a bit ambitious maybe a more lightweight construct might work like the concept of Dictionaries in Python which are used to store data values in key:value pairs. > For classical topological spaces people care about homotopies and > homology. Homology for simplicial complexes essentially reduces to > linear algebra over integers, so is relatively easy. First homotopy > group is in general uncomputable. Assuming that first homotopy > group is trivial, there is old result about higher homotopy groups, > namely there is relation to homology of loop spaces. Loop spaces > as normally defined are not simpilical complexes, but it is > relatively easy to give infinite simpilical complex which is > homotopy equvalent to loop space of a simplical complex. So > one needs to tame infinity. One step here was done by E. Brown, > who proved that to compute homotopy of given order is is enough > to look at finite part of infinite simpilical complex equivalent > to loop space. Complex given by Brown is quite large. F. Sergeraert > showed that one can use much smaller finite complex, which allowed > practical computations. AFAICS there is rather heavy theory > behind this and implementation needs a lot of coding. > > Vector bundles over simplicial complexes have rather natural > representation: over each simplex you have vector space > of given dimension, so by choosing basis you can just take > R^n. On intersection of simplexes there is change of base, > so you need a transition matrix. In general this transition > matrix may be an arbitrary continous matrix function, subject > to agreement rules. But you should be able to do with > matrix valued polynomials (or rational functions since we need > inverses). And AFAICS homotopic sets of transition matrices > give isomorphic bundles, so there is more possibilities to > limiot form of transition matrices. If transition matrices > take values in orthogonal matrices you should be able to > represent bundles of spheres in similar way. If transition > matrices have integer entries and determinant +-1 you will > get bundles of toruses. > > In somewhat different direction you may consider algebraic > sets. CAD (implementd by CylindricalAlgebraicDecompositionPackage) > give you decomposition of real algebraic set into cells, > so you should be able to produce a simplicial complex from > such decomposition. If the set is smooth you may consider > tanget bundle or normal bundle. > > I think that analog of cylindrical algebraic decomposition > works for more general sets, defined by elementary equations > and inequalities (with reasonable regularity assumptions needed > to avoid uncomputability). But again, this probaly would > require working out details of theory (I am not aware of > precise description) and coding is likely to be rather > involved. > > I would suggest to start with relatively simple things and > make them work well, so simplicial complexes rather than > generalizations, functions which are as simple as possible > (for mappings one gets nontrivial theory already from > piecewise linear maps). Are you saying that the existing simplicial complex code in alg_top.spad needs reworking? I would like to improve this and add simplicial sets (like simplicial complex but based on a weak order). Before I look at this I want to learn more about the fundamentals of finite topological spaces and implement some code for that. I am interested in the link to cylindrical algebraic decomposition you mention so I will investigate that more and see if it can be linked to the structures in alg_top.spad or new topology code. I assume there are no tutorials for the CAD package? Also I will try to find out more about the loop spaces you mention. My personal motivation is to learn more about these powerful and beautiful mathematical structures and if any code that comes out of that is useful to others that would also be good. I find self study difficult when text books have exercises to prove something and I get stuck. Since programs have similarities to proofs (in a Curry-Howard sort of way) I find it better to work with code. At least programs are easier to debug than proofs. The ultimate example of this would be if I could implement Homotopy Type Theory or Cubical Type Theory in FriCAS (I know that's an impossible goal). Martin -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/8b65fdd7-ab19-4f6a-b9c0-c53887031218%40martinb.com.
