How can I find the dependencies at the Table of Contents level?

[Anarcocap-socdem]

Hello, I would like to understand the dependencies at the Table of Contents level. For this, I mean that I would like to see the Metamath follows a "tree of mathematics" structure, whereby logic and ZFC are at the roots, and then (possibly, this is what I want to confirm) there are three stems out of the roots, the numbers, algebra and topology. And then, these three stems have their own leaves, which in fact, are very often leaves with origins in more than one stem (topology and the numbers are required for analysis, geometry, probability ...).

Of course, I could go by myself, go deep into the ToC, and check for myself if my assumption is true or not (especifically, that there are no "hidden" dependencies, meaning that in fact there are more, or less, stems at the origin). And of course, I will try to do it. But maybe I could have some help from the experts here, since maybe there is a way to check what I am saying in an easier (and safer) way.

Note: this tree of mathematics that I am referring one is a very specific one, with no history or no "common sense" order, like for example, saying that geometry is one of the stems of mathematics (which conceptually is true, since geometry has been one of the key forces in "doing mathematics" throughout the millenia, but in "metamath" sense, geometry is way, way higher in the tree, and less "basic", I assume).

Thanks!

[Mario Carneiro]

We do not make any serious attempt to make the dependency structure nonlinear, so every later section can refer to any previous section. Between sections and parts this is less common simply because the subject matters are different, but there are no hard rules there.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6f739681-df49-4c8b-943c-2dfd3e2343a3%40googlegroups.com.

[Thierry Arnoux]

Hi Jordi,

Even if they are developed independently, at some point, both Topology and Algebra join again for topologic-algebraic structures, like Hilbert spaces.

There was this very interesting post by Mattia Morgavi, who drew a graph based on relations between Metamath theorems in set.mm:

https://groups.google.com/forum/#!msg/metamath/uFXl6ogSDyQ/2SxbhqFzCwAJ

However, it's not visible from his graph whether there are dependencies between Algebra and Topology or not...

Note that in set.mm our "early definition" of the complex numbers as a structure with both algebraic and topological properties also forces us to pull some topological definitions earlier than they are really needed.

BR,
_
Thierry

[Thierry Arnoux]

PS. Regarding your question, the most interesting picture from Mattia's post may be this one:

https://01463712226776492098.googlegroups.com/attach/b73a1865b2cd9/Graph4.png?part=0.2&view=1&vt=ANaJVrHCraV7Lgu6NW4LjwDKXcZwOb5y2X2uJ_BELhOb4UcsnjdDgjPg15K-sRObNkY6KYQNBWk0hiHNneA9-NYRzNxjqztTfh4fCxvOgJNh0-WQMoxTZoU

It shows both theorems about Algebraic and Topological structures on the same picture.

In my eyes, on this graph, the most interesting theorems will be those bridging otherwise unrelated regions. I'm curious which they are.

(And sorry for the double posting)