论文标题
Orbifolds作为合成差分凝聚力类型理论的微连续性类型
Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory
论文作者
论文摘要
在非正式的情况下，Orbifold是一个光滑的空间，其点可能具有许多内部对称性。但是，正式地，Orbifold的概念已经以多种不同的态度（从Satake的V-Manifolds到Moerdijk和Pronk的适当的Étalegropsoids）提出，它们的脸上不像非正式的定义。形式主义和直觉之间这种差异的原因是，空间的点不能在传统的设定级基础中具有内部对称性。这些对称性的额外数据必须在整个理论中随身携带并解释。更明显的是，以通常方式呈现的Orbifold之间的地图不能点上定义。 在本文中，我们将提出一个合成差分凝聚同型理论的Orbifold的定义：Orbifold是一种微连续性类型，任何两个点之间的识别类型都是适当有限的。在同型类型理论中，一种类型的点可能具有内部对称性，我们将能够通过直接定义其点的类型来构建Orbifolds的示例。此外，两个Orbifolds之间的映射空间仅仅是函数的类型。 我们将通过内部证明每个适当的典型群体都是Orbifold来证明这种综合定义的合理性。通过这种方式，我们将证明综合理论忠实地扩展了通常的Orbifolds理论。在此过程中，我们将研究较高类型的诸如étalegroupoids的微连接性，表明合成差异几何形状的方法优雅地推广到平滑空间的更高类似物。我们还将研究合成差异几何形状中的dubuc-penon与紧凑性的开放式覆盖定义之间的关系，并表明任何离散的，dubuc-penon的紧凑型子集的第二个可容纳歧管的紧凑型子集均可列举。
Informally, an orbifold is a smooth space whose points may have finitely many internal symmetries. Formally, however, 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. The extra data of these symmetries must be carried around and accounted for throughout the theory. More drastically, maps between orbifolds presented in the usual ways cannot be defined pointwise. In this paper, we will put forward a definition of orbifold in synthetic differential cohesive homotopy type theory: an orbifold is a microlinear type for which the type of identifications between any two points is properly finite. In homotopy type theory, a point of a type may have internal symmetries, and we will be able to construct examples of orbifolds by defining their type of points directly. Moreover, the mapping space between two orbifolds is merely the type of functions. We will justify this synthetic definition by proving, internally, that every proper étale groupoid is an orbifold. In this way, we will show that the synthetic theory faithfully extends the usual theory of orbifolds. Along the way, we will investigate the microlinearity of higher types such as étale groupoids, showing that the methods of synthetic differential geometry generalize gracefully to higher analogues of smooth spaces. We will also investigate the relationship between the Dubuc-Penon and open-cover definitions of compactness in synthetic differential geometry, and show that any discrete, Dubuc-Penon compact subset of a second-countable manifold is subfinitely enumerable.
