Интерпретируются ли типы идентичности физически в бесконечно-топосной формулировке уравнений движения?

Ссылаясь на статью/книгу Урса Шрайбера об основах теории поля « Дифференциальные когомологии в связном топосе бесконечности », я задаюсь вопросом: используются ли там тождественные типы «только» для вычислений или они сами в какой-то момент интерпретируются как представляющие некоторую физическую величину? Могу ли я думать о «пространствах пути» как о чем-то более конкретном? (изменить: запрос ссылки в комментариях: тип удостоверения в nLab.)

Это то, что изначально реализовано в логике, и мне интересно, становятся ли они затем в геометрической структуре привязанными к некоторым более конкретным интуитивным понятиям. И я имею в виду уровень, выходящий за рамки того факта, что эти гомотопии, возможно, уже являются визуальными и, следовательно, физическими. Я имею в виду, что это похоже на то, как утверждение, что гамильтониан является функцией энергии, дает физикам больше понимания, чем просто заявление о том, что это функция в фазовом пространстве, порождающая траектории.

Итак, скажем по-другому: из всего логического языка, который HoTT предоставляет с самого начала, что из этого становится чем- то физическим/чем-то в мире?

@Trimok: я добавил ссылку. Это (тип, как в программировании) есть утверждение о равенстве двух вещей. С вычислительной точки зрения это набор обоснований этого утверждения. В HoTT оно тоже геометрическое — это пространство путей» я → М «. Я пытался понять типы идентичности как подмножества наборов хомов в вопросе на доске по математике, и этот ответ может быть полезен. Если вы читаете это, давайте удалим этот список комментариев здесь.
У вас нет никакой информации в главе 5 (Приложения) (со страницы 577 ) архивной статьи Урса Шрайбера ?
@Trimok: я теряю идентичность на стр. 200, когда он вводит типы, но подчеркивает связь с более категоричным языком. Физика появляется на стр. 387. Я ожидал, что поля являются термами типа продукта, а типы идентичности над ними — калибровочными эквивалентностями . На стр. 397 у него есть таблица с эквивалентностями между физически «разумными» вещами и понятиями (связного) HoTT, но там я вижу только эквивалентности (они могут быть просто тождественными по одновалентности или около того). Но правда в том, что я даже не знаю, что и думать, когда вижу Б .
Является Б по отношению к понятию классификационных пространств , например классификационное пространство для U(n) ?
@Trimok: Да, предположительно. Но это еще не все, так как я также видел типичных людей, бросающих столицу Б вокруг, которые, как оказалось, даже не знали, что такое касательное пространство Т М является. Я даже не знаю, как интерпретировать, если с этой стороны. Я полагаю, что геометрический аспект этой теории может быть решен только с помощью теории гомотопических типов, но, как было сказано выше, я не знаю, какая часть новизны этой теории на самом деле входит в работу Шрейбера — на первый взгляд, текст кажется хорошо работающим. topoi, не знаю, как новый материал на самом деле влияет на него, поэтому я и спрашиваю.
@Trimok: связь с пакетами неудивительна, как и при переписке Карри Ховарда , для логического предиката Е (например Е ( Икс ) "=" " Икс четно") у вас есть это предложение ∀ ( Икс е Икс ) . Е ( Икс ) пишется как зависимый тип Π ( Икс : Икс ) . Е ( Икс ) , где каждый Е ( Икс ) является типом. И доказательство с предложения или с : Π ( Икс : Икс ) . Е ( Икс ) , присваивает каждому Икс 0 : Икс доказательство с ( Икс 0 ) из Е ( Икс 0 ) . В геометрической интерпретации с является сечением расслоения, где Е это волокна над Икс с.
Возможно, у вас будет больше ответов, если вы поменяете теги и поставите: квантовая теория поля, исследовательский уровень, математическая физика.
Хотя я еще недостаточно углубился в статью Урса, чтобы ответить (и вряд ли у меня будет много времени, чтобы продолжить в ближайшие месяцы), вы, возможно, захотите перейти к сообщению Дэвида Корфилда о кафе n-категории о Бумага Урса и направьте их на ваш вопрос. Вероятно, в разделе комментариев есть несколько человек, которые могут вам помочь.

Ответы (1)

Вот запоздалый ответ. (С этим вопросом я столкнулась только сейчас, случайно. Это было опубликовано как раз, когда родилась наша дочь, что немного отвлекло меня...)

Быстрым ответом на вопрос является следующее несколько примечательное утверждение.

Примечательно, что когда теория гомотопических типов оснащена дополнительной аксиомой дифференциального сцепления , тогда можно «дифференцировать» типы идентичности. Их бесконечно малая версия — известные из калибровочной теории БРСТ-комплексы . А точнее: «призрак» в БРСТ-комплексе — это касательная к терму в тождественном типе, призрак-призраков — касательная к терму в тождественном-типе-тождественного-типа и т. д. .

Можно сказать так: теория гомотопических типов — это новое основание математики, в которое встроен калибровочный принцип . Калибровочный принцип в том смысле, что неправильно спрашивать, равны ли две конфигурации поля, мы должны спросить, существует ли калибровочная эквивалентность, связывающая их. И если таких больше одного, то неправильно спрашивать, равны ли два калибровочных преобразования, вместо этого мы должны спрашивать, есть ли между ними калибровочное преобразование, и так далее.

Поэтому, когда вы спрашиваете, как типы идентичности отражают «что-то в мире», вам просто нужно искать случаи, когда калибровочные преобразования имеют мирское воплощение. Примеров конечно масса. Рассмотрим теорию инстантонов и вспомним, что стандартная теория КХД утверждает, что вакуум, в котором мы живем, представляет собой море инстантонов, где на фемтометр приходится примерно один инстантон. Это означает, что физическая реальность, в которой мы живем, если убрать все и просто рассмотреть простой вакуум, уже плотно заполнена, если хотите, физическим воплощением типов идентичности.

В общем, в этом и состоит основа физики в высшей геометрии/высшей теории топосов/теории гомотопических типов: корректно учитывать не только пертурбативные эффекты, но и учитывать полную непертурбативную структуру калибровочной теории, все «большие» калибровочные преобразования, все квантовые аномалии, все глобальные эффекты. Геометрическая гомотопическая теория (стеки с более высокими модулями) является математическим языком для этого, и приятное понимание Владимира Воеводского и других состоит в том, что это, в свою очередь, имеет глубокую синтаксическую / логическую формулировку в теории гомотопических типов.

Заметьте, никто об этом не просил, это подарок, данный нам природой: можно было бы заподозрить, что чем глубже мы погружаемся в математическую структуру современной локальной калибровочной квантовой теории поля, тем она становится все более сложной, все более изощренной. : стеки модулей, дифференциальные когомологии, аномалии и т. д. Но в свете теории гомотопических типов обнаруживается, что поразительно, как только мы добираемся до ее основания, то внезапно в основаниях калибровочной квантовой теории поля все становится концептуально проще ., в смысле "простой красоты" в законах физики. Например, в когезионной теории гомотопических типов есть элегантный способ прямо говорить о искривленной дифференциальной K-теории, лежащей в основе устранения аномалий Фрида-Виттена в 2d КТП. Он просто вытекает из основополагающих аксиом в нескольких шагах, а не представляет собой длинную запутанную конструкцию, которая появлялась в исследовательских статьях (здесь я имею в виду материал, относящийся к разделу 4.1.2 ).

Я мог бы продолжить, но, возможно, мне следует остановиться здесь. Если моя книга кажется длинной, попробуйте следующие два текста, которые призваны быстро показать путь от голых основ когезионной теории гомотопических типов к локальной лагранжевой теории калибровочных полей:

Спасибо за ответ, я работаю, чтобы понять это. Я полагаю, вы хотели бы увидеть мой дополнительный вопрос , который более конкретен.
Зачем нужны типы» "=" " для начала? В конце концов, теория слабых категорий может обойтись без нее. Можете ли вы указать мне, почему в HoTT мы начинаем с типа идентичности, а затем навязываем ( А "=" Б ) ≃ ( А ≃ Б ) ? Скажем, мы начинаем с зависимо типизированной теории (с ∏ , ∑ в частности), а затем определить " ≃ " как это сделано в книге HoTT. Если принцип эквивалентности Т М должна быть реализована с помощью этой аксиомы, почему мы в первую очередь рассматриваем теорию с тождеством. Похоже, все, что мы действительно хотим, это «просто» эквивалентность. Кстати. Я тащусь на nForum - есть раздел вопросов?
Или позвольте мне сказать: я понимаю потребность в пространствах путей, но нужно ли нам «собственное равенство», прежде чем мы определим эквивалентность и тем самым получим желаемое понятие равенства?
Да, определение "≃" включает "=". Функция является эквивалентностью тогда и только тогда, когда все ее гомотопические слои стягиваемы, а для того, чтобы сказать «гомотопический слой» и «стягивается», используется «=». В моделях это понимается так: «=» видит морфизмы внутри объекта бесконечности-категории, а «≃» видит морфизмы самой бесконечности-категории. Теперь есть классификатор объектов, который представляет собой маленькое изображение целой категории внутри себя. Таким образом, в этом конкретном объекте отражаются оба вида морфизмов, и аксиома однолистности говорит, что они совпадают. Итак, внутреннее и внешнее согласны.
Вы можете задавать вопросы на nForum. Просто нажмите «Начать обсуждение» в левом верхнем углу, выберите соответствующую категорию обсуждения, обычно «Атриум: математика, физика и философия», и вперед.
Интерпретируются ли типы идентичности физически в бесконечно-топосной формулировке уравнений движения?
СпросиСетьПолитика конфиденциальности1y, 0v