Your profile says you are a PhD Candidate, so perhaps you are interested in some more details. Also maybe this answer is a bit off-topic and a bit overly advertising! But I found the things below extremely helpful for my own understanding how mathematics can be structured (digitally).
I would like to elaborate on user87690's answer. They are correct that your diagram treats obvious inclusions, e.g. Vectorspace $\hookrightarrow$ NormedVectorSpace, in the same way as non-obvious "inclusions", e.g. TopologicalSpace $\hookrightarrow$ MetricSpace. Let me introduce you to the the theoretical side of some very general framework called MMT, which is able to exactly capture all those cases of "blah induces blub". In one sentence, one could say MMT is a scalable module system for mathematical knowledge management. Knowledge is organized into MMT theories and MMT morphisms (or short morphisms) -- but we'll get to this. Let's first start where your post ended.
(Disclaimer: I have contributed to and written about MMT in the past. However, I'd dare to say that the things you'll hopefully learn below will easily convert over to other mathematical knowledge management systems. They all have a notion of modules and interconnection between modules.)
Generalized Inclusions
The generalization of inclusions are so-called MMT morphisms written as $\rightsquigarrow$, e.g. $$\text{TopologicalSpace} \rightsquigarrow \text{MetricSpace}.$$ You can read this as "any metric space induces a topological space". The same holds true for ordinary inclusions $\hookrightarrow$, e.g. $$\text{VectorSpace} \hookrightarrow \text{NormedVectorspace}$$ can also be read as "every normed vectorspace induces a vectorspace", but it's special insofar that a normed vectorspace is the same as a vectorspace with additional things -- norms and norm axioms.
With this notation, I can give you a new picture:
Note that there is no arrow from $\text{BanachSpace}$ to $\text{InnerProductSpace}$ precisely because the latter is not necessarily complete. Hence an incomplete inner product space cannot induce a Banach space, which is complete by the very definition!
I'd like to remark that one can compose MMT morphisms. For example, we can obtain a morphism $\text{TopologicalSpace} \rightsquigarrow \text{HilbertSpace}$ by composition! It would translate to your diagram as follows: if a box $B$ is in a box $C$, and the box $C$ is in a box $D$, then $B$ is also in $D$.
What do MMT morphisms look like?
Until know I only told you how we could conveniently make use of that $\rightsquigarrow$ notation without telling you how it is really defined. For that we first have to define in between what this arrow actually is. What are its domain and codomain? They are MMT theories.
Theories
An MMT theory captures a specific mathematical theory. More precisely, it can list its signatures, axioms, theorems and proofs. All these notions are subsumed by so-called (typed) declarations. Essentially, theories are nothing else than list of such declarations. You can also think of the declarations as specifying a language for you to talk in.
Let me provide a running example. It'll be a bit easier than the mathematical theories you had in your diagram. Particularly, let us walk through the following assertion: $$\text{Monoid} \rightsquigarrow \text{NaturalNumbers}$$
Recall, this means that "natural numbers form a monoid". I assume you know what a monoid is: it's a set $U$ equipped with a binary associative operation $op: U \times U \to U$ and a neutral element $e \in U$. We've just identified three declarations we would formalize for the domain theory in MMT. Indeed, the formalization looks as follows:
theory Monoid =
U: type ❙
e: U ❙
op: U ⟶ U ⟶ U ❙
❚
I'll skip over some details, but you can recognize the same $U$, $e$ and $op$, right? Perhaps read $U \to U \to U$ as $U \times U \to U$. If you're interested, this is the same by currying. So far so good! (You might rightly remark that I skipped the associativity and neutrality axioms. Indeed, I did. You can add them in a very similar way via the propositions-as-types idiom/Curry-Howard correspondende.)
Let's continue with the natural numbers, the codomain of our morphism. They look as follows:
theory NaturalNumbers =
ℕ: type ❙
0: ℕ ❙
successor: ℕ ⟶ ℕ ❙
plus: ℕ ⟶ ℕ ⟶ ℕ ❙
❚
We have the actual symbol $\mathbb{N}$, declare a zero symbol $0$, a successor function and finally a plus function.
Morphisms
Remember we wanted to make a formal version of our assertion $$\text{Monoid} \rightsquigarrow \text{NaturalNumbers}.$$ Now I finally can tell you what MMT morphisms are. Such a morphism $\varphi: S \rightsquigarrow T$ is a list of assignments: for every declaration $s \in S$ we have to give an assignment $\varphi(s)$, which is a $T$-expression. Let's see how the above envisioned morphism looks like:
view σ : Monoid -> NaturalNumbers =
U = ℕ ❙
e = 0 ❙
op = plus ❙
❚
You can replace the word view by morphism in your head. I am just sticking to the official syntax. That's it! This tells us that natural numbers form a monoid in the following sense:
- we take their universe set $U$ precisely as $\mathbb{N}$,
- we take the neutral element as $0$,
- and we take the binary operation as plus.
Multiple Morphisms
One nice aspect of our generalization is that we can also express multiple inductions. Consider this:
- the natural numbers form a monoid wrt. $0$ and $+$
- the natural numbers form a monoid wrt. $1$ and $\cdot$
We already did the first bullet point above! Can you see how we would do the second one?
Overall, it's not enough to say that "natural numbers form a monoid". We must say how. Precisely by giving a concrete mapping -- a morphism. Often we omit this if there is only one obvious canonical morphism. For a different example, you might consider in which ways a Hilbert space might induce a topological space. Ever heard of the weak topology? :)
One more complex example
To conclude this introduction to MMT, I'll provide one more complex morphism, namely the one $$\text{MetricSpace} \rightsquigarrow \text{NormedVectorspace}.$$ I'll omit the code for involved (co)domain theories for brevity. Just imagine the domain had a declarataion $X: type$ for its universe and a declaration $d: X \to X \to \mathbb{R}$ for its metric. Similarly, imagine the codomain theory had a declaration $Y: type$ for its universe and -- among others -- a $norm: Y \to \mathbb{R}$ function as well as a subtraction function denoted by $-$. Then the morphism code would look as follows:
view σ : MetricSpace -> NormedVectorspace =
X = Y ❙
d = [y1: Y, y2: Y] norm (y1 - y2) ❙
❚
You can read […] as (typed) lambda binders. So we assign to $d$ the anonymous function $Y \to Y \to \mathbb{R}$ with $y_1 \mapsto \left(y_2 \mapsto \lVert y_1 - y_2 \rVert\right)$.
Where to go from here?
Having formalized theories and morphisms allows us working with mathematical knowledge, especially auto-generating visualizations. Have a look at a TGView3D demo view and its corresponding arXiv article.
If you have further interest, you can
I am more than happy to answer questions if you have any :)
