KIT | KIT-Bibliothek | Impressum
Open Access Logo
DOI: 10.5445/IR/1000073164

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.

Zugehörige Institution(en) am KIT Institut für Algebra und Geometrie (IAG)
Publikationstyp Hochschulschrift
Jahr 2017
Sprache Englisch
Identifikator URN: urn:nbn:de:swb:90-731648
KITopen ID: 1000073164
Verlag Karlsruhe
Umfang 95 S.
Abschlussart Dissertation
Fakultät Fakultät für Mathematik (MATH)
Institut Institut für Algebra und Geometrie (IAG)
Prüfungsdatum 12.07.2017
Referent/Betreuer Prof. F. Herrlich
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page