Geometry in Modal HoTT 2019
Подяка за підтримку
Як завжди перед початком звітом по конференції хочу висловити подяку усім, хто підтримує мене на тернистому шляху докторантури. В першу чергу це моя родина та друзі, які надихають мене, а також представники академії які допомогають мені у цьому. Окрім моїх покровителів з КПІ, перш за все — це звичайно усі спікери та учасники конференції "Геометрія в модальнії Гомотопічній теорії типів". Також хотів би подякувати усім моїм клієнтам, які з розумінням ставляться до моєї математичої діяльності та не відволікають мене по дрібницям.
Передісторія
Як ви знаєте конструктивна теорія типів HoTT відкриває дорогу в CW-комплекси та алгебраїчну топологію, однак значний пласт проблем вона не вирішує, наприклад теоерема Брауера про нерухому точку не виводиться у цій теорії, те саме стосується таких речей як етальні відображення, на яких будується фундамент сучасної диференціальної геометрії. Модальна теорія HoTT у пов'язаних топосах зародилася як продукт дослідження Урсом Шрайбером Картанової супергеометрії у застосуванні до сучасної теоретичної фізики та було детально розроблена як розширення HoTT Майком Шульманом (cohesivett). Після дисертації Фелікса Велена стало зрозуміло, що HoTT у зв'язаних топосах може вирішити останні проблеми формалізації математики і ця конференція перший івент цього штибу.
Еґберт Райке
Еґберт захистив свій мастер тезис у Андрія Бауера, а дисертацію у Стів Еводі. Але найбільше Еґберт вплинув на мене своїм курсом по HoTT. Усього є декілька курсів: по-перше це сам підручник з HoTT, далі курс Валерія Ісаєва, курс Роберта Харпера (15-819), та один з найбільш просвітлюючих курсів це HoTT курс Еґберта, про який я писав на каналі Групоїд Інфініті. Його курс найбільше вплинув на мій власний курс HoTT.
Також Еґберт відомий тим, що у співробітництві з Ульріком Бушхольцом формалізував квартерніонні фібрації Хопфа. На цьому воркшопі Еґберт представив зразу три доповіді. Перша було про рефлексивні підсвествіти та модальності, де показав, що транкейшин рівні гомотопічних типів є рефлексивними підвсесвітами, їх універсальні властивості, необхідні умови доступності для підвсесвітів, еквівалентність визначень локальних відображень, локальних просторів, та замкненість підвсесвітів відносно еквівалентностей. Друга доповідь була присвячена відокремленим просторам (простір L-відокремлений, якщо усі його id-типи L-локальні, де L — рефлективний підвсесвіт). Тут розлядалось чи завжди підвсесвіт L-відокремлених типів є рефлексивним підвсесвітом. Третя доповідь була про Модальний спуск та рефлексивні системи факторизації, де були дані визначенння ортогональних систем факторизації (ОFS), стабільних OFS, та n-етальні відображення..
Майк Шульман
Переоцінити вклад Майкла Шульмана в розвиток HoTT важко. Фактично він основним автором ncatlab Cafe, співзасновником ncatlab, та головним контрибутором в cohesivett, теорію яка відкрила двері в математику нескінченних околів, та інших модальностей, яка були ним розроблена з подачі Урса Шрайбера. На ції конференції Майк Шульман представив дві доповіді. Перша була присвячена основам теорії звязанних топосів (про яку вперше можно прочитати у Вільяма Лавіра). В першій доповіді були дані основні визначення комонадичної флет-модальності (бемоль) згідно з принципами MLTT (формації, інтро, елімінатори, бета та ета рівності), яка за якою власне і схована корекурсія обчислення нескінченно малих величин, або більше відомих в математиці як епсилон-околи. Це база cogesivett, розробка якої розпочалася в далекому 2011 році. Також було обговорення імплементації бемоль модальності в Agda (flat-бренч на гітхабі). Друга доповідь була присвячена семантиці вищих молальностей, та за допомогою бемоль-модальності була накінець-то конструктивно доведена теорема Брауера про нерухому точку (яка як відомо не доводиться у чистій HoTT), чим було закрито кон'юнктуру Еводі, у залі стояли гучні аплодисменти. Раджу усім послухати цю доповідь, хто скептично ставився до конструктивної математики.
Урс Шрайбер
Урс один з засновників сучасної математичної енциклопедії ncatlab, якою користуються усі сучасні математики, не тільки в області інфініті категорій, HoTT, а також прикладної та теоретичної фізики, яка для Урса є головним мотиватором. Вперше ідея запропонувати cohesive топоси Лавіра для моделювання вищих геометорій та логік виходила саме від Урса, а Майк Шульман виконова усю необхідну роботу по формалізації (cohesivett). Як бачимо колаборація Майка та Урса виходять далеко за межі адмінітративної роботи по управлінню математичної екнциклопедії ncatlab, якою ми з вами зачитуємося до 5-ї години ранку.
Додовання модальностей як системи операторів до HoTT дає змогу дуже елегатно доводити теореми вищої геметрії, диференціальної топології, диференціальної гемометрії, супергеметрії. В доповіді Урса показані засади Картанової геометрії, формальної Картанової геометрії та Картанової Супергеометрії. Головна мотивація для Урса — це побудова формальної М-теорії (спільна робота з Хішамом Саті в Нью-Йоркському Університеті в Абу Дабі). Урс побудував вежу модальностей які хитро вилаштовуються в діагональ спряжень, і чи має ця вежа кінець відкрите питання в новоспеченій модальній HoTT.
Нижній рядок — Empty та Unit, другий рядок модальностей застосовується в диференціальній топології (ретопологізація та топологізація) — шейп модаліті, флет (бемоль) модаліті, та шарп (дієз) моділіьті, третій рядок застосовується у диференціальній геометрії (Im та Re модальності), та верній рядок — фізика (бозонні та ферміонні модальності), далі вежа насичується та стабілізується (начебто?). Синім кольором зображені мотивні локалізації афінного відрізка.
Як на мене це сама езотерична теорія сучасної формальної математики та теоретичної фізики яка дає безмежне натхнення по формальнізації будь яких теорії (М-теорія, теорія струн, супергеометрія, інші версії гомотопічних теорій). Без сумніву Урса можна назвати батьком модальної гомотопічної теорії типів, а також батьком ncatlab!
Фелікс Веллен
Фелік Веллен перший учень Урса Шрайбера який детально розробив у своїй дисертації Im модальності, які застосовуються для моделювання етальних відображень, які у свою чергу дозволяють доводити теореми про нескінченнін околи (диференціальна геометрія). Сама дисертація Фелікса відрила у мене друге дихання та породила нову лінію сайтів-брендів etale.space та sheaf.space. Власне цей воркшоп присвячений геометрій відбувся завдяки зусиллям Фелікса, як головного організатора заходу.
Ульрік Башхольтц
У Ульріка багато регалій, але якби мене попросили його описати одним досягненням, то я би сказав, що Ульрік єдина людина у світі яка змогла формалізувати кватерніонне розшарування Хопфа (мова Lean). Також я замовив у Ульріка code review інтерналізації кубічної теорії у мову Lean (Ground Zero), так як Ульрік адепт Lean.
Доповідь Ульріка була присвячена некомутативній теорії когомологій, а саме пучкам (gerbe, як інструмент гокомологій степені 2), крученням (twist), лєнтам (band). І усе це в модальній HoTT. Дивіться його підручник з симетрій Symmetry Book
Пітер Арндт
Пітер Арндт представив абстраткну мотивну теорія гомотопій — яка є одночасно його PhD тезисом. Доповідь почалася зі зведеної теорії когомологій як функтора з оберненої категорії топологічних просторів з точками в абелеву категорію: Top*op -> AbZ. Далі були розглянуті схеми на базою К: K-Alg -> Set. Потім ми розглянули глядкі схеми та мотивні простори з топологією Нісневича/Заріського, мотивні спектри та мотиви HZ-Mod (шестикутник). Потім ми замінили мотивні простори на представимі інфініті декартово замкнені категорії та визначили таким чином цілком абстрактну мотивну теорію гомотопій. Були розглянуть стабільні та нестабільні результати та побудови та наведені достатні приклади. Показана можливість пабудови раціонального оператора Адамса.
В другій частні доповіді були рознлянуті гладкі спектри, орієнтовані теорії когомологій, обчислення ендоморфізмів, спектри Мореля, модальна версія An-гомотопічної теорії, групоїди Пікара, мотивна теорема Воєводського та шифіфікація.
Спонтанне інтерв'ю з авторами кубіків
Нагадаю, що кубіками я називаю системи доведення теорем, які побудовані на базі кубічної теорії типів, єдиної теорії типів, у якій можно довести аксіому унівалентності Воєводського. 5 із шести кубічних тайпчекері були написані в CMU цими хлопцями (три версії на мові хаскель: cubicaltt, cubicaltt/hcomptrans, yacctt, одна на Standard ML — RedPRL, та одна на OCaml). Не взяти інтерв'ю в авторів цих пруверів було би великою необачністю. Я зробив презентацію нашої бібліотеки Groupoid Infinity — усі були у захваті.
Андерс Мортберг
Не знажаючи на те, що cubicaltt більше не розроблюється, Андерс жартує, що він ідеальний, тому нема далі що покращувати. Наймінімальніший синтаксис кубічної теорії який поміщається на 12-рядках BNF нотації!
Карло Анджіулі, Джон Стерлінг
Джон Стерлінг пропрацював деякий час в індустрії програмного забепечення, тому його системи відрізняються дорослістю та сккладністю. Карло забезпечує математичну підтримку, але усі вони программісти та математики, важно виділити що головніше!
Еван Кавалло
Еван був представлений мені як спеціаліст з вищих індуктивних типів (CW-комплексів), або HIT-чарівник! Останні публікації стосовно теорії HIT та формалізація тайпчекінга HIT в декартовій кубічній теорії — заслуги Евана.
Стів Еводі
Стіва Еводі можна назвати батьком гомотопічної теорії типів (HoTT), саме на запрошення Стіва Володимир Воєводський почав інтенсивно займатися HoTT, а також завдяки Стіву відбувся проект HoTT. Як хранитель та модератор Стів спостерігав за конференцією та був адвайзором багатьох людей присутніх на конференції.
Перелік абстрактів усіх доповідей разом зі слайдами та відео.
Далі буде.