KIT | KIT-Bibliothek | Impressum | Datenschutz

Formalizing Cartan Geometry in Modal Homotopy Type Theory

Wellen, Felix

Abstract (englisch):

Both, the category of smooth manifolds and the category of schemes may be faithfully embedded in categories of (higher) sheaves on appropriate sites. Homotopy Type Theory is used to reason about those objects and following a suggestion from Urs Schreiber, a modality given by axioms, is used to access the differential geometric structure of the sheaves.
This allows the definition of a notion of infinitesimal proximity, admitting intuitive reasoning on the type theory side. A theorem which forms the basis of what could be called Cartan Geometry is proven, generalizing classical theorems for smooth manifolds. Morphism properties resembling the notions of formally étale, smooth and unramified morphisms from Algebraic Geometry are derived from the notion of infinitesimal proximity and used to define and study spaces locally modeled on a class of types subsuming infinity-groups, vectors spaces and H-spaces. This culminates in the definition of torsion free G-structures.

Volltext §
DOI: 10.5445/IR/1000073164
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Algebra und Geometrie (IAG)
Publikationstyp Hochschulschrift
Publikationsjahr 2017
Sprache Englisch
Identifikator urn:nbn:de:swb:90-731648
KITopen-ID: 1000073164
Verlag Karlsruher Institut für Technologie (KIT)
Umfang 95 S.
Art der Arbeit Dissertation
Fakultät Fakultät für Mathematik (MATH)
Institut Institut für Algebra und Geometrie (IAG)
Prüfungsdatum 12.07.2017
Referent/Betreuer Herrlich, F.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page