David Jaz Myers: "A synthetic approach to orbifolds"

Topos Institute Colloquium, 8th of September 2022. ——— Orbifolds are smooth spaces where the points may have finitely many internal symmetries. These spaces often arise as quotients of manifolds by the actions of discrete groups --- that is, in situations with discrete symmetries, such as in crystallography. Formally, the notion of orbifold has been presented in a number of different guises -- from Satake's V-manifolds to Moerdijk and Pronk's proper étale groupoids -- which do not on their face resemble the informal definition. The reason for this divergence between formalism and intuition is that the points of spaces cannot have internal symmetries in traditional, set-level foundations. In this talk, we will see a formal definition which closely tracks the informal idea of an orbifold. By working with the axioms of synthetic differential geometry in cohesive homotopy type theory, we will give a synthetic definition of orbifold (subsuming the traditional definitions) which closely resembles the informal definition: an orbifold is a microlinear type where the type of identifications between any two points is properly finite. In homotopy type theory, we can construct these orbifolds simply by giving their type of points.