Teoría del tipo de homotopía: ¿qué es?

Question

Mi pregunta es, en términos generales, ¿cuál es el principal proyecto de Homotopy Tipo de Teoría (HoTT). Le pregunté a un profesor que es probable que sea correcta y dice lo siguiente:

Hay tres direcciones:

1. Topologists están viendo el tipo de teoría como una forma concisa y formas convenientes de la razón acerca de la topología, donde las igualdades son interpretados como rutas de acceso (y de mayores dimensiones variantes de la misma).
2. Tipo de teóricos están viendo topología como una manera de obtener nuevos conocimientos sobre el tipo de teoría y variantes de los mismos.
3. La gente está empujando univalence y tipo constructivo de la teoría como un nuevo fundamentos de las matemáticas.

El único de los que he agarre es 2. A mi entender, obtenido a partir de algunas charlas que yo no entiendo es como sigue:

Algunas personas le gustaría escribir una prueba de comprobación/generación de cliente que es lo suficientemente expresivo para que usted realmente puede hacer matemáticas en ella. La manera de conseguir este alto nivel de expresividad es a través de una muy rica tipo de teoría.

Nos dimos cuenta de que usted podría intepret estos tipos topológicamente: un objeto es un punto, una prueba de que la igualdad es un camino, una prueba de que dos pruebas de la igualdad son "el mismo" es un homotopy.

Ahora, la gente usa los atractivos de la modelo, para orientar el desarrollo de la prueba de medio ambiente, que es aproximadamente el punto 2.

De alguna manera, sin embargo, hay una esperanza de que usted puede utilizar este sistema para calcular homotopy grupos de esferas? ¿Por qué es esto creíble?

También, esto está siendo promovida como una nueva fundación? Por qué? ¿Qué ventajas tiene sobre la teoría de conjuntos?

Answer 1

La descripción de las tres direcciones no es demasiado malo, aunque no son, por supuesto, totalmente independiente, ni tampoco todo lo que se llama HoTT caer en uno de ellos. También, no estoy seguro de si esto se aplica a usted, pero yo siempre señalar que es potencialmente confuso para decir "topología", cuando lo que se quiere decir es "homotopy teoría", es decir, "$\infty$- groupoid teoría" — todos los "espacios" aparecen en HoTT sólo hasta homotopy.

Algunas personas le gustaría escribir una prueba de comprobación/generación de cliente que es lo suficientemente expresivo para que usted realmente puede hacer matemáticas en ella.

No estoy seguro de lo que el uso de una prueba de comprobación de programa sería si no podía hacer matemáticas en... (-:

Pero sí, creo que su descripción del punto 2 es aproximadamente correcta. El punto 1 es sólo acerca de la utilización del modelo en la otra dirección: si usted demostrar algo en el tipo de teoría, entonces es cierto, como una declaración acerca de los espacios. En particular, si usted calcular algo así como un homotopy grupo de una esfera en el tipo de teoría, entonces es también una verdadera declaración acerca de la homotopy grupos de esferas en la clásica topología algebraica. Y, de hecho, lo hemos hecho en un par de casos simples, como $\pi_n(S^n)$ e $\pi_3(S^2)$, por lo que es mejor debe ser creíble. Estas pruebas son diferentes, desde el clásico y elegante, a la que, en cierto sentido, y relativamente fácil formalizable en una prueba de asistente. (Aviso que yo estoy hablando acerca de las diferentes pruebas de resultados conocidos aquí; no es inconcebible que los nuevos métodos de HoTT podría conducir a pruebas de nuevos resultados, incluso en el clásico homotopy teoría, pero espero que ese día está lejos en el futuro).

Como para el punto 3, tipo de teoría, en general, tiene un montón de ventajas sobre la teoría de conjuntos como una base para las matemáticas. Entre otras cosas, se requiere menos arbitraria "codificación" para representar las matemáticas, que se asemeja más a la práctica de matemáticas, y puede ser más fácil de programar en una computadora, la producción de pequeña "prueba" de plazo certificados que pueden ser fácilmente verificado. UF/HoTT potencialmente corrige algunas de las desventajas de tipo tradicional teoría, tales como la falta de buen comportamiento de los cocientes y el problema de transporte de las estructuras a través de las equivalencias, por lo que es aún mejor. Y además de las tradicionales de las matemáticas, que también incluye nuevas matemáticas, tales como la "sintético homotopy teoría" en los cálculos de homotopy grupos mencionados anteriormente.

Finalmente, un punto que siempre me destacar: HoTT tiene muchos modelos de otras que el "estándar" en los espacios. Aproximadamente podemos usar cualquier "$(\infty,1)$-topos" (aunque hay coherencia preguntas todavía un trabajo en progreso). Esto significa que a la hora de probar algo en UF/HoTT (tales como homotopy grupo de cálculo, o cualquier parte de la tradicional de las matemáticas que podríamos formalizar la utilizan como una fundación) el resultado es más general que en el clásico homotopy teoría, ya que es cierto que en cualquiera de los modelos.