TU Darmstadt / ULB / TUbiblio

A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects

Weinberger, Jonathan (2022)
A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects.
Technische Universität Darmstadt
doi: 10.26083/tuprints-00020716
Dissertation, Erstveröffentlichung, Verlagsversion

Kurzbeschreibung (Abstract)

Reasoning about weak higher categorical structures constitutes a challenging task, even to the experts. One principal reason is that the language of set theory is not invariant under the weaker notions of equivalence at play, such as homotopy equivalence. From this point of view, it is natural to ask for a different foundational setting which more natively supports these notions.

A possible approach along these lines has been given by Riehl–Shulman in 2017 where they have developed a theory of synthetic (∞,1)-categories. For this purpose they have introduced an extension of homotopy type theory/univalent foundations (HoTT/UF). Pioneered by Voevodsky, this logical system is designed to develop homotopy theory in a synthetic way, meaning that its basic entities can essentially be understood as topological spaces, or more precisely homotopy types. As per Voevodsky's Univalence Axiom, homotopy equivalence between types coincides with logical equivalence. As a consequence, a lot of the conceptual ideas from classical homotopy theory can be imported to reason more intrinsically about homotopical structures.

In fact, in 2019 Shulman achieved to prove the long-standing conjecture that any higher topos (in the sense of Grothendieck–Rezk–Lurie) gives rise to a model of homotopy type theory. This gives a precise technical sense in which HoTT can be regarded as a kind of internal language of (∞,1)-toposes ℰ. By analogy, Riehl–Shulman's extension, called simplicial homotopy type theory (sHoTT), can be interpreted in diagram (∞,1)-toposes of the form ℰ^(Δ^op). Syntactic additions make it possible to reason type-theoretically about internal (∞,1)-categories implemented as (complete) Segal objects.

Based on Riehl–Shulman's work about synthetic (∞,1)-categories and discrete covariant fibrations, we present a theory of co-/cartesian fibrations including sliced and two-sided versions. The study is informed by Riehl–Verity's work on model-independent ∞-category theory, and transfers results of their ∞-cosmoses to the type-theoretic setting. We prove characterization theorems for cocartesian fibrations and their generalizations, given as existence conditions of certain adjoint functors (Chevalley criteria). Extending the author's previous joint work with Buchholtz, we prove several closure properties of two-sided cartesian fibrations as well as a two-sided Yoneda Lemma. Furthermore, we discuss so-called Beck–Chevalley (bi)fibrations and prove a synthetic (∞,1)-categorical version of Moens' Theorem, after Streicher.

Finally, we show how to interpret Riehl–Shulman's strict extension types in the intended higher topos model, in such a way that makes them strictly stable under substitution. This uses a method, originally due to Voevodsky, which has previously been employed in the works of e.g. Kapulkin, Lumsdaine, Warren, Awodey, Streicher, and Shulman.

Our work takes up on suggestions in the original article by Riehl–Shulman to further develop synthetic (∞,1)-category theory in simplicial HoTT, including in particular the study of cocartesian fibrations. Together with a collection of analytic results, notably due to Riehl–Verity and Rasekh, it follows that our type-theoretic account constitutes a synthetic theory of fibrations of internal (∞,1)-categories.

Typ des Eintrags: Dissertation
Erschienen: 2022
Autor(en): Weinberger, Jonathan
Art des Eintrags: Erstveröffentlichung
Titel: A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects
Sprache: Englisch
Referenten: Streicher, Prof. Dr. Thomas ; Riehl, Prof. PhD Emily ; Berg, Prof. PhD Benno van den
Publikationsjahr: 2022
Ort: Darmstadt
Kollation: xxi, 177 Seiten
Datum der mündlichen Prüfung: 9 Dezember 2021
DOI: 10.26083/tuprints-00020716
URL / URN: https://tuprints.ulb.tu-darmstadt.de/20716
Kurzbeschreibung (Abstract):

Reasoning about weak higher categorical structures constitutes a challenging task, even to the experts. One principal reason is that the language of set theory is not invariant under the weaker notions of equivalence at play, such as homotopy equivalence. From this point of view, it is natural to ask for a different foundational setting which more natively supports these notions.

A possible approach along these lines has been given by Riehl–Shulman in 2017 where they have developed a theory of synthetic (∞,1)-categories. For this purpose they have introduced an extension of homotopy type theory/univalent foundations (HoTT/UF). Pioneered by Voevodsky, this logical system is designed to develop homotopy theory in a synthetic way, meaning that its basic entities can essentially be understood as topological spaces, or more precisely homotopy types. As per Voevodsky's Univalence Axiom, homotopy equivalence between types coincides with logical equivalence. As a consequence, a lot of the conceptual ideas from classical homotopy theory can be imported to reason more intrinsically about homotopical structures.

In fact, in 2019 Shulman achieved to prove the long-standing conjecture that any higher topos (in the sense of Grothendieck–Rezk–Lurie) gives rise to a model of homotopy type theory. This gives a precise technical sense in which HoTT can be regarded as a kind of internal language of (∞,1)-toposes ℰ. By analogy, Riehl–Shulman's extension, called simplicial homotopy type theory (sHoTT), can be interpreted in diagram (∞,1)-toposes of the form ℰ^(Δ^op). Syntactic additions make it possible to reason type-theoretically about internal (∞,1)-categories implemented as (complete) Segal objects.

Based on Riehl–Shulman's work about synthetic (∞,1)-categories and discrete covariant fibrations, we present a theory of co-/cartesian fibrations including sliced and two-sided versions. The study is informed by Riehl–Verity's work on model-independent ∞-category theory, and transfers results of their ∞-cosmoses to the type-theoretic setting. We prove characterization theorems for cocartesian fibrations and their generalizations, given as existence conditions of certain adjoint functors (Chevalley criteria). Extending the author's previous joint work with Buchholtz, we prove several closure properties of two-sided cartesian fibrations as well as a two-sided Yoneda Lemma. Furthermore, we discuss so-called Beck–Chevalley (bi)fibrations and prove a synthetic (∞,1)-categorical version of Moens' Theorem, after Streicher.

Finally, we show how to interpret Riehl–Shulman's strict extension types in the intended higher topos model, in such a way that makes them strictly stable under substitution. This uses a method, originally due to Voevodsky, which has previously been employed in the works of e.g. Kapulkin, Lumsdaine, Warren, Awodey, Streicher, and Shulman.

Our work takes up on suggestions in the original article by Riehl–Shulman to further develop synthetic (∞,1)-category theory in simplicial HoTT, including in particular the study of cocartesian fibrations. Together with a collection of analytic results, notably due to Riehl–Verity and Rasekh, it follows that our type-theoretic account constitutes a synthetic theory of fibrations of internal (∞,1)-categories.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Der Umgang mit schwachen unendlichdimensionalen Kategorien stellt selbst für Expert*innen eine Herausforderung dar. Dies begründet sich schon auf grundsätzlicher Ebene damit, dass die Sprache der Mengenlehre nicht invariant unter den Äquivalenzbegriffen dieser schwachen, höherdimensionalen Strukturen ist, wie z.B. Homotopieäquivalenz. Unter diesem Gesichtspunkt ist es naheliegend, nach einer alternativen Grundlagentheorie zu suchen, die mit den homotopietheoretischen Begriffen besser kompatibel ist.

Ein möglicher Ansatz wurde 2017 von Riehl–Shulman in Form einer synthetischen Theorie von (∞,1)-Kategorien vorgeschlagen. Zu diesem Zweck haben sie eine Erweiterung der sogenannten Homotopie-Typentheorie bzw. univalenten Grundlagen (engl. homotopy type theory/univalent foundations (HoTT/UF)) eingeführt. Hierbei handelt es sich um ein logisches System, entscheidend geprägt durch Wojewodski, das eine synthetische Grundlage für Homotopietheorie bieten soll: Die grundlegenden Objekte tragen bereits eine topologische Struktur. Genauer gesagt, handelt es sich um Homotopietypen. Wojewodskis Univalenz-Axiom bewirkt, dass in diesem System Homotopieäquivalenz mit logischer Äquivalenz übereinstimmt. Dies hat zur Folge, dass viele konzeptionelle Ideen aus der klassischen Homotopietheorie benutzt werden können, um eine synthetische Theorie aufzubauen.

Ein entscheidender Beitrag wurde 2019 von Shulman geleistet, der bewies, dass jeder höherdimensionale Topos (im Sinne von Grothendieck–Rezk–Lurie) Anlass zu einem Modell von Homotopie-Typentheorie gibt. Diese Vermutung war lange Zeit offen. Nach diesem Resultat kann man HoTT in einem genauen technischen Sinne als eine Art interne Sprache beliebiger (∞,1)-Topoi ℰ verstehen. Analog dazu lässt sich Riehl–Shulmans Erweiterung, die sog. simpliziale Homotopietypentheorie (sHoTT), in Diagramm-(∞,1)-Topoi der Form ℰ^(Δ^op) interpretieren. Vermöge syntaktischer Erweiterungen erlaubt die Theorie die Behandlung interner (∞,1)-Kategorien, modelliert durch sogenannte (vollständige) Segal-Objekte.

Ausgehend von Riehl–Shulmans Arbeit über synthetische (∞,1)-Kategorien und diskrete kovariante Fibrationen entwickeln wir eine Theorie ko-/kartesischer Fibrationen, die auch gefaserte und zweiseitige Verallgemeinerungen erfasst. Dabei dienen Riehl–Veritys Arbeiten über modellunabhängige (∞,1)-Kategorientheorie als wichtige Grundlage, deren Resultate für ∞-Kosmoi wir auf den typentheoretischen Kontext übertragen. Wir geben Charakterisierungssätze für kokartesische Fibrationen und ihre Verallgemeinerungen an, die als Existenzsätze bestimmter adjungierter Funktoren formuliert sind (Chevalley-Kriterien). Gemeinsame Vorarbeiten mit Buchholtz verallgemeinernd zeigen wir eine Auswahl von Abschlusseigenschaften zweiseitiger kartesischer Fibrationen sowie ein zweiseitiges Yoneda-Lemma. Desweiteren diskutieren wir sogenannte Beck–Chevalley-(Bi-)Fibrationen und beweisen eine synthetische (∞,1)-kategorielle Version des Satzes von Moens, basierend auf einem Beweis von Streicher.

Abschließend führen wir eine Kohärenzkonstruktion für Riehl–Shulmans strikte Erweiterungstypen durch, sodass diese auch in den homotopietheoretischen Topos-Modellen strikt substitutionsstabil interpretiert werden können. Diese Methode geht auf Wojewodski zurück und fand Anwendung in Arbeiten von z.B. Kapulkin, Lumsdaine, Warren, Awodey, Streicher und Shulman.

Unsere Arbeit folgt Vorschlägen aus dem ursprünglichen Artikel von Riehl–Shulman, die synthetische (∞,1)-Kategorientheorie in simplizialer Homotopie-Typentheorie weiterzuentwickeln, insbesondere bezüglich kokartesischer Fibrationen. Zusammen mit einer Reihe analytischer Resultate, v.a. von Riehl–Verity und Rasekh, folgt aus den genannten Betrachtungen, dass unser typentheoretischer Zugang eine synthetische Theorie von Fibrationen interner (∞,1)-Kategorien darstellt.

Deutsch
Status: Verlagsversion
URN: urn:nbn:de:tuda-tuprints-207163
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 500 Naturwissenschaften und Mathematik > 510 Mathematik
Fachbereich(e)/-gebiet(e): 04 Fachbereich Mathematik
04 Fachbereich Mathematik > Logik
Hinterlegungsdatum: 24 Feb 2022 14:42
Letzte Änderung: 02 Mär 2022 09:20
PPN:
Referenten: Streicher, Prof. Dr. Thomas ; Riehl, Prof. PhD Emily ; Berg, Prof. PhD Benno van den
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 9 Dezember 2021
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen