Tu perfil dice que eres un estudiante de Doctorado, así que tal vez usted está interesado en más detalles. También tal vez la respuesta a esto es un poco off-topic y un poco demasiado de la publicidad! Pero me he encontrado con lo siguiente extremadamente útil para mi propia comprensión de cómo las matemáticas pueden ser estructurados (digitalmente).
Me gustaría explicar user87690 la respuesta. Están en lo correcto de que su diagrama de trata inclusiones obvio, por ejemplo, Vectorspace $\hookrightarrow$ NormedVectorSpace, de la misma manera como no evidentes "inclusiones", por ejemplo, TopologicalSpace $\hookrightarrow$ MetricSpace. Permítame que le presente a la parte teórica de algunos marco muy general llamado MMT, que es capaz de exactamente la captura de todos los casos de "bla induce blub". En una frase, se podría decir que el MMT es una solución escalable el sistema de módulo para la gestión de los conocimientos matemáticos. El conocimiento está organizado en MMT teorías y MMT morfismos (o corto morfismos) -- pero vamos a llegar a esto. Primero vamos a empezar por donde tu post terminado.
(Descargo de responsabilidad: he contribuido a y escrito acerca de MMT en el pasado. Sin embargo, me atrevería a decir que las cosas que te esperamos aprender de abajo va a convertir fácilmente a otros matemáticos de sistemas de gestión del conocimiento. Todos ellos tienen una noción de los módulos y la interconexión entre los módulos.)
Generalizada Inclusiones
La generalización de las inclusiones son los llamados MMT morfismos escrito como $\rightsquigarrow$, por ejemplo, $$\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:
![New theory graph with adapted notation of inclusions (\hookrightarrow) and general MMT morphisms (\rightsquigarrow)]()
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}$$
Recordar, esto significa que "los números naturales forman un monoid". Supongo que usted sabe lo que es un monoid: es un conjunto $U$ equipado con un binaria asociativa de operación $op: U \times U \to U$ y un elemento neutro $e \in U$. Hemos identificado tres declaraciones queremos formalizar para el dominio de la teoría en la MMT. En efecto, la formalización se ve de la siguiente manera:
theory Monoid =
U: type ❙
e: U ❙
op: U ⟶ U ⟶ U ❙
❚
Voy a omitir algunos detalles, pero se puede reconocer el mismo $U$, $e$ e $op$, ¿verdad? Tal vez leer $U \to U \to U$ como $U \times U \to U$. Si usted está interesado, este es el mismo por alarmada. Tan lejos y tan bien! (Puede que con razón, la observación de que me he saltado la asociatividad y la neutralidad de los axiomas. De hecho, lo hice. Usted puede agregar en una forma muy similar a través de las propuestas-como-tipos de lenguaje/Curry-Howard correspondende.)
Vamos a seguir con los números naturales, el codominio de nuestro morfismos. Se ven de la siguiente manera:
theory NaturalNumbers =
ℕ: type ❙
0: ℕ ❙
successor: ℕ ⟶ ℕ ❙
plus: ℕ ⟶ ℕ ⟶ ℕ ❙
❚
Tenemos el símbolo $\mathbb{N}$, declarar un cero símbolo $0$, una función sucesor y, finalmente, un plus de función.
Morfismos
Recuerde que quería hacer una versión formal de nuestra afirmación $$\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}$,
- tomamos el elemento neutro como $0$,
- y tomamos la operación binaria como plus.
Varios Morfismos
Un aspecto positivo de nuestro generalización es que también se puede expresar de varias inducciones. Considere esto:
- los números naturales forman un monoid wrt. $0$ e $+$
- los números naturales forman un monoid wrt. $1$ e $\cdot$
Ya hicimos la primera viñeta de arriba! Se puede ver cómo podríamos hacer el segundo?
En general, no es suficiente para decir que "los números naturales forman un monoid". Debemos decir cómo. Precisamente por dar un hormigón de asignación -- una de morfismos. A menudo se omite esta opción si sólo hay una evidente canónica de morfismos. Para otro ejemplo, usted podría considerar la posibilidad de que formas un espacio de Hilbert, podrían inducir a un espacio topológico. Has oído hablar de la topología débil? :)
Un ejemplo más complejo
Para concluir esta introducción a la MMT, voy a ofrecer una más compleja de morfismos, a saber, el $$\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: tipo de$ for its universe and a declaration $d: X \X \to \mathbb{R}$ for its metric. Similarly, imagine the codomain theory had a declaration $Y: tipo$ for its universe and -- among others -- a $norma: 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 \a Y \to \mathbb{R}$ with $y_1 \mapsto \left(y_2 \mapsto \lVert y_1 - y_2 \rVert\right)$.
A dónde ir desde aquí?
Haber formalizado teorías y morfismos nos permite trabajar con el conocimiento matemático, especialmente la auto-generación de visualizaciones. Eche un vistazo a un TGView3D demo de vista y su correspondiente arXiv artículo.
Si usted tiene interés, puede
Estoy más que feliz de contestar preguntas si usted tiene alguna :)
