¿Se interpretan físicamente los tipos de identidad en una formulación topos infinita de ecuaciones de movimiento?

En referencia al artículo / libro de Urs Schreibers sobre los fundamentos de la teoría del campo Cohomología diferencial en un topos infinito cohesivo, me pregunto: ¿los tipos de identidad se usan "solo" para los cálculos, o se interpretan en algún momento para representar alguna cantidad física? ¿Puedo pensar en los "espacios de ruta" como algo más concreto aquí? (editar: solicitud de referencia en los comentarios: tipo de identidad en el nLab.)

Son lo que se implementa de forma nativa en la lógica y me pregunto si, luego en el marco geométrico, estos se vinculan a algunas nociones intuitivas más concretas. Y me refiero a un nivel más allá del hecho de que podría decirse que las homotopías ya son visuales y, por lo tanto, físicas. Lo digo de manera similar a cómo decir que el hamiltoniano es la función de energía da más información a los físicos que simplemente decir que es una función en el espacio de fase, generando caminos.

Dicho de otra manera: de toda la lingua lógica que ofrece HoTT desde el principio, ¿qué se convierte en algo físico/algo en el mundo?

@Trimok: He agregado un enlace. Es (el tipo, como en programación) es la proposición de igualdad de dos cosas. Desde un punto de vista computacional, es la colección de justificaciones para esta proposición. En HoTT también es geométrico, es un espacio de camino " I → METRO ". Traté de entender los tipos de identidad como sub"conjuntos" de conjuntos de hom-set en una pregunta en el tablero de Matemáticas y esta respuesta podría ser útil. Si lee esto, eliminemos esta lista de comentarios aquí.
no tienes informacion en el capitulo 5 (Aplicaciones) (de la página 577 ) del artículo arxiv de Urs Schreiber ?
@Trimok: pierdo la noción de las identidades alrededor de la página 200 cuando presenta tipos pero enfatiza la conexión con el lenguaje más categórico. La física parece aparecer en la p.387. Lo que hubiera esperado al entrar en esto es que los campos son términos de un tipo de producto y los tipos de identidad sobre estos son las equivalencias de calibre . En la página p.397 tiene una tabla con equivalencias entre cosas físicamente "razonables" y nociones de HoTT (cohesivo), pero allí solo veo equivalencias (podrían ser simplemente identitas por univalencia, más o menos). Pero la verdad es que ni siquiera sé muy bien qué pensar cuando veo un B .
Es B en relación con la noción de espacios de clasificación , por ejemplo, espacio de clasificación para U(n) ?
@Trimok: Sí, probablemente. Pero hay más, ya que también he visto personas afines al tipo tirando la capital B alrededor, que resultó no saber siquiera lo que es un espacio tangente T METRO es. Ni siquiera sabría cómo interpretarlo desde este lado. Me imagino que el aspecto geométrico podría salvarse solo a través de la teoría del tipo de homotopía, pero como se dijo anteriormente, no sé cuánto de la novedad de esa teoría realmente entra en el trabajo de Schreibers; a primera vista, el texto parece funcionar con agradable topoi, no estoy seguro de cómo las cosas nuevas realmente lo influyen, y es por eso que pregunto.
@Trimok: la conexión con los paquetes no es sorprendente como en la correspondencia de Curry Howard , para un predicado lógico mi (p.ej mi ( X ) := " X es par") tienes que la oración ∀ ( X ∈ X ) . mi ( X ) se escribe como tipo dependiente Π ( X : X ) . mi ( X ) , donde cada mi ( X ) es un tipo Y y una prueba s de la proposición, o s : Π ( X : X ) . mi ( X ) , asigna a cada X 0 : X una prueba s ( X 0 ) de mi ( X 0 ) . En la interpretación geométrica, s es una sección de la fibración, donde el mi 's son las fibras más X 's.
Tal vez tenga más respuestas cambiando sus etiquetas y poniendo, teoría del campo cuántico, nivel de investigación, física matemática
Aunque no he avanzado lo suficiente en el artículo de Urs para responder (ni es probable que tenga mucho tiempo para ir más allá en los próximos meses), es posible que desee dirigirse a la publicación de café de categoría n de David Corfield sobre El papel de Urs y apúntelos hacia su pregunta. Es probable que haya algunas personas en la sección de comentarios que puedan ayudarte.

Respuestas (1)

Aquí hay una respuesta tardía. (Me encontré con esta pregunta solo ahora, por casualidad. Esto se publicó justo cuando nació nuestra hija, lo que me distrajo un poco...)

La respuesta rápida a la pregunta es la siguiente declaración un tanto notable

En particular, cuando la teoría del tipo de homotopía está equipada con el axioma adicional de cohesión diferencial , entonces uno puede "diferenciar" los tipos de identidad. Su versión infinitesimal son los complejos BRST famosos de la teoría de gauge. O más bien: un "fantasma" en un complejo BRST es una tangente a un término en un tipo de identidad, un fantasma de fantasmas es una tangente a un término en un tipo-identidad-de-un-tipo-identidad y así sucesivamente .

Se podría decir de esta manera: la teoría del tipo de homotopía es una nueva base de las matemáticas que tiene incorporado el principio de calibre . El principio de calibre en el sentido de que: es incorrecto preguntar si dos configuraciones de campo son iguales, tenemos que preguntar si existe una equivalencia de calibre que las relacione. Y si hay más de una, entonces es incorrecto preguntar si dos transformaciones de calibre son iguales, en lugar de eso, debemos preguntar si hay una transformación de calibre entre ellas, y así sucesivamente.

Entonces, cuando pregunta cómo los tipos de identidad se reflejan en "algo en el mundo", solo necesita buscar casos en los que las transformaciones de calibre tengan una encarnación mundana. Los ejemplos, por supuesto, abundan. Considere la teoría de los instantones y recuerde que la teoría QCD estándar dice que el vacío en el que habitamos es un mar de instantes con aproximadamente un instante por femtómetro. Esto significa que la realidad física que habitamos, si eliminas todo y consideras simplemente el vacío, ya está densamente llena, si lo deseas, con la encarnación física de los tipos de identidad.

En general, de esto se trata la base de la física en geometría superior/teoría del topos superior/teoría del tipo de homotopía: tener en cuenta correctamente no solo los efectos perturbadores, sino tener en cuenta la estructura no perturbativa completa de la teoría de calibre, todos las transformaciones de calibre "grandes", todas las anomalías cuánticas, todos los efectos globales. La teoría de la homotopía geométrica (pilas de módulos superiores) es el lenguaje matemático para hacerlo, y la idea agradable de Vladimir Voevodsky y otros es que esto, a su vez, tiene una formulación sintáctica/lógica profunda en la teoría de tipos de homotopía.

Tenga en cuenta que nadie pidió esto, este es un regalo que nos ha dado la naturaleza: habría sospechado que cuando profundizamos cada vez más en la estructura matemática de la teoría cuántica de campo de calibre local moderna, se vuelve cada vez más complicado, cada vez más sofisticado. : pilas de módulos, cohomología diferencial, anomalías, etc. Pero a la luz de la teoría del tipo de homotopía, uno encuentra que, sorprendentemente, a medida que uno va realmente al fondo de la misma, luego, de repente, en los fundamentos de la teoría cuántica de campo de calibre, de repente las cosas se vuelven conceptualmente más simples ., en el sentido de "belleza simple" en las leyes de la física. Por ejemplo, en la teoría del tipo de homotopía cohesiva hay una manera elegante de hablar directamente de la teoría K diferencial torcida que está en el corazón de la cancelación de anomalías de Freed-Witten en 2d QFT. Simplemente está fluyendo en unos pocos pasos desde los axiomas fundamentales, en lugar de ser la construcción larga e intrincada que ha aparecido en los artículos de investigación (aquí me estoy refiriendo a cosas relacionadas con la sección 4.1.2 ).

Podría seguir, pero tal vez debería detenerme aquí. Si mi libro parece largo, pruebe con los siguientes dos textos que están destinados a mostrar rápidamente el camino desde los fundamentos básicos de la teoría del tipo de homotopía cohesiva hasta la teoría del campo de calibre de Lagrangian local:

Gracias por la respuesta, estoy trabajando para entenderlo. Me imagino que le gustaría ver mi pregunta de seguimiento , que es más concreta.
¿Por qué necesitamos tipos? = " para empezar? Después de todo, la teoría de la categoría débil puede prescindir de ella. ¿Puede señalarme por qué, en HoTT, comenzamos con un tipo de identidad y luego imponemos ( A = B ) ≃ ( A ≃ B ) ? Digamos que empezamos con una teoría tipada de forma dependiente (con ∏ , ∑ en particular) y luego definir " ≃ como se hace en el libro HoTT. Si el principio de equivalencia T METRO debe implementarse con este axioma, ¿por qué consideramos una teoría con identidad en primer lugar? Parece que todo lo que realmente queremos es equivalencia "solo" de todos modos. Por cierto. Acecho el nForum - ¿hay una sección de preguntas?
O permítanme decir: entiendo la necesidad de espacios de ruta, pero ¿necesitamos "igualdad propiamente dicha" antes de definir la equivalencia y obtener así la noción deseada de igualdad?
Sí, la definición de "≃" implica "=". Una función es una equivalencia si y solo si todas sus fibras de homotopía son contráctiles, y para decir "fibra de homotopía" y "es contráctil" se usa "=". En los modelos esto se entiende como: "=" ve los morfismos dentro de un objeto de categoría infinita, pero "≃" ve los morfismos de la categoría infinita misma. Ahora está el clasificador de objetos, que es una pequeña imagen de toda la categoría dentro de sí misma. Entonces, en ese objeto en particular, se reflejan ambos tipos de morfismos y el axioma de univalencia dice que concuerdan. Así que lo interno y lo externo están de acuerdo.
Le invitamos a hacer preguntas en el nForum. Simplemente presione "Iniciar una discusión" en la parte superior izquierda, seleccione una categoría de discusión adecuada, generalmente "Atrium: Matemáticas, Física y Filosofía", y continúe.
¿Se interpretan físicamente los tipos de identidad en una formulación topos infinita de ecuaciones de movimiento?
RespuestasAquíPolítica de privacidad1y, 0v