首页/论文/1606.06540

arXiv 1606.065402016-06math.CT

同伦型理论I中的合成differential geometry

Synthetic differential geometry within homotopy type theory I

Hirokazu Nishimura

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文给出了第一步发展综合微分几何同伦型理论。它的模型论将在随后的论文中讨论。

英文摘要：

This paper gives a first step towards developing synthetic differential geometry within homotopy type theory. Its model theory will be discussed in a subsequent paper.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

同伦型理论：高阶等式的综合方法

Homotopy Type Theory: A synthetic approach to higher equalities

这是对同伦类型理论和哲学家的单价基础的介绍，作为《工作哲学家的范畴》一书的一章（伊莱恩·兰德里编辑）。

2016-01-27math.CTmath.LO

模态同伦类型论中的合成G-射流结构

Synthetic G-jet-structures in modal homotopy type theory

本文在带单子模态的同伦类型论中构造无挠G-射流结构的模叠，适用于配稳定分解系统的∞-拓扑空间，以低复杂度表述并提供形式化，分解系统可由deRham-Stack构造给出。

2024-12-04math.AGmath.CTmath.DG

de Rham同伦理论与微分分次范畴

The de Rham homotopy theory and differential graded category

本文是arXiv：0810.0808的推广。我们开发的德拉姆同伦理论不一定幂零空间，使用封闭的DG-范畴和等变DG-代数。我们看到这两个代数对象以某种方式相对应。证明了图式同伦类型的同伦范畴与闭dg-范畴的同伦范畴之间的等价性。本文用极小模型刻画了空间的同伦不变量。在这种情况下，极小模型的行为很像沙利文的极小模型。我们还提供了一些例子。我们证明了纤维合理化和封闭的dg范畴与辅助数据之间的等价性。

2011-08-23math.ATmath.CT

概率规划同伦类型论中的综合拓扑

Synthetic topology in Homotopy Type Theory for probabilistic programming

ALEA Coq库基于集合范畴上的Giry monad的变体形式化了测度理论。这使得解释概率程序设计语言与原语从离散分布采样。然而，连续分布必须离散化，因为相应的措施不能定义在所有子集的载波。本文提出了使用合成拓扑建模连续分布的概率计算类型论。研究了任意集合上的初始$σ$ -框架和相应的诱导拓扑.基于这些内在的拓扑结构，我们定义的估值和低积分集，并证明版本的Riesz和Fubini定理。然后，我们将展示如何勒贝格估值，因此连续分布，可以构建。

2021-06-25cs.LOmath.CT

同伦类型论：空间逻辑

Homotopy type theory: the logic of space

这是从范畴论和拓扑学的角度对类型论、合成拓扑学和同伦类型论的介绍，作为《数学和物理的新空间》（Gabriel Catren和Mathieu Anel编）一书的一章。

2017-03-08math.CTmath.LO

合成微分凝聚同伦类型理论中的微线性轨道折叠

Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory

非正式地，一个orbifold是一个光滑的空间，其点可能有许多内部对称。然而，在形式上，轨道折叠的概念已经以许多不同的形式提出-从佐竹的V-流形到Moerdijk和Pronk的proper étale groupoid-它们表面上不像非正式定义。形式主义和直觉之间这种分歧的原因是，在传统的集合层次基础中，空间的点不可能具有内部对称性。这些对称性的额外数据必须在整个理论中被携带和解释。更重要的是，以通常方式表示的轨道之间的映射不能逐点定义。本文在综合微分凝聚同伦类型论中给出了轨道折叠的定义：轨道折叠是指任何两点之间的同一性类型为真有限的微线性类型。在同伦类型论中，一个类型的点可能具有内部对称性，我们将能够通过直接定义点的类型来构造轨道褶皱的例子。此外，两个轨道之间的映射空间仅仅是函数的类型。我们将证明这个综合定义的合理性，通过内部证明，每个真的代数广群是一个轨道。这样，我们将表明，综合理论忠实地扩展了通常的orbifold理论。在此过程中，我们将研究更高类型的微线性，如étale广群胚，表明综合微分几何的方法优雅地推广到光滑空间的更高类似物。我们还将研究在综合微分几何中紧性的Dubuc-Penon和开覆盖定义之间的关系，并证明第二可数流形的任何离散的Dubuc-Penon紧子集都是次可积的。

2022-05-31math.ATmath.CTmath.DG

更多相关论文收起更多论文

合成 ∞-范畴的极限与余极限

Limits and colimits of synthetic $\infty$-categories

University of Ottawa（渥太华大学）

本文在合成 simplicial 同调类型理论框架下，研究了 ∞-范畴的极限与余极限理论，并展示了空间族的极限可通过依赖积计算。

2024-07-25math.CT

同伦类型论中的离散微分几何

Discrete differential geometry in homotopy type theory

本文在同伦类型论中基于单纯复形定义了主丛、联络、曲率和向量场等微分几何构造，并证明了一个关联总曲率与总指数的定理，为证明 Gauss-Bonnet 定理和 Poincaré-Hopf 定理奠定关键基础。

2025-04-29math.CTmath.DG

稳定性同调论中结合律的障碍

Obstructions for Associativity in Stable Homotopy Theory

本文通过构造稳定性∞-范畴中A_n-代数结构的障碍理论，展示谱S/4通过合成谱具有A_5乘法。

2026-05-12math.ATmath.CT

离散群下同调理性同调理论的代数模型

Algebraic models for equivariant rational homotopy theory for discrete groups

Universidad de Málaga（马拉加大学）；University of Warsaw（华沙大学）

本文提出一种框架，将空间同调理论的代数模型推广到真正的equivariant情况。讨论了交换微分格雷德代数模型和完备微分格雷德李代数模型在有理空间中的应用，并与其他模型类别进行比较。

2026-08-05math.ATmath.CT

同伦类型论作为图示的∞-逻辑格的语言

Homotopy type theory as a language for diagrams of $\infty$-logoses

Stockholms universitet（斯德哥尔摩大学）

论文展示通过扩展同伦类型论加入某些lex可及模态量，可将∞-逻辑格的图示重构，从而用普通同伦类型论处理单个或多个∞-逻辑格。

2026-03-10cs.LOmath.CTmath.LO

图的凝聚模型：有理同伦中的混合Hodge结构

Cofibrant models of diagrams: mixed Hodge structures in rational homotopy

我们研究了一类顶点在具有函子路径的可变范畴中的图范畴的同伦理论，从而得到了关于凝聚对象的同伦范畴的一个很好的计算。将这一理论应用到微分分次代数的混合Hodge图范畴中。利用Sullivan的极小模型，我们证明了混合Hodge复形上Beilinson定理的一个乘法形式.作为结果，我们得到了有理同伦型复代数簇上的混合Hodge结构的函性。在这种情况下，由Morgan理论得到的同伦群上的混合Hodge结构是由混合Hodge图的不可分解的导出函子得出的。

2013-07-18math.ATmath.CT

单纯同伦类型论中的广义Chevalley准则

Generalized Chevalley criteria in simplicial homotopy type theory

本研究在Riehl–Shulman单纯同伦类型论框架下，将（余）笛卡尔箭头、纤维化与函子的经典条件推广为以任意形状包含替代端点包含的广义形式，为合成内蕴$(\u221e,1)$-范畴论研究提供了新的处理方式。

2024-03-13cs.LOmath.ATmath.CT

有向同伦类型论

Towards a directed homotopy type theory

在本文中，我们提出了一个有向同伦类型论综合推理（高）类，有向同伦理论，及其应用并发。我们指定一个新的“同态”型前的马丁-洛夫类型论，这是大致类似的身份型前最初介绍的马丁-洛夫。同态类型形成器是用来捕捉态射（来自范畴理论）和有向路径（来自有向同伦理论）的概念，就像单位类型形成器是用来捕捉同构（来自群胚理论）和路径（来自同伦理论）的概念一样。我们的主要结果是这些同态类型的猫，范畴的小范畴的解释。在那里，每个同态类型hom（a，b）的解释确实是范畴C的对象a和b之间的态射集合。最后，我们分析了猫的解释，我们认为，我们的同态类型确实是有向版本的马丁-洛夫的身份类型。

2018-07-27cs.LOmath.CT

合成differential geometry中的一些微分方程

Some differential equations in synthetic differential geometry

一些微分方程被认为是在综合微分几何的背景下。这里，这意味着不仅利用了幂零无穷小，而且利用了函数空间的形成。特别是，我们利用分布空间在我们的研究波和热方程。

2001-04-17math.CTmath.DG

作为谱层的微分上同调理论

Differential cohomology theories as sheaves of spectra

我们证明了，在一个稳定的（无穷大，1）-范畴（如谱或链复形）的值的光滑流形的网站上的每一个层产生一个微分上同调图和同伦公式，这是微分上同调理论的所有经典例子的共同特征。这些结构自然是从一个规范分解成一个同伦不变量的一部分和一块，其中有一个平凡的评价点的层。在经典的例子中，后者是微分形式的贡献。这种分解提出了一种自然的方案，通过确定这些碎片和胶合数据来分析新的层。我们进行这种分析的各种经典和不那么经典的例子。

2013-11-13math.ATmath.CTmath.KT

通过一元和共元模态合成光谱

Synthetic Spectra via a Monadic and Comonadic Modality

我们扩展同伦类型理论与一个新的模态，同时是单子和comonad。因为这种模态在每一个类型上都诱导了一个非平凡的内映射，所以它需要一个比同伦类型论以前的模态扩展更复杂的判断结构。我们使用这个理论来开发一种光谱的合成方法，其中光谱由某些类型表示，并且通过类型结构来构建它们：谱的映射由普通函数表示，闭路空间由单位类型表示，等等。我们用一对公理扩充了类型论，其中一个公理意味着谱是稳定的，另一种是把合成谱与类型论中谱的普通定义联系起来，称为$Ω$ -谱。最后，我们表明，类型理论是健全的和完整的抽象范畴语义，在范畴与家庭的弱自同态函子的上下文中是一个双反射，即有一个counit一个单位，是一个部分收缩对。

2021-02-08math.ATmath.CTmath.LO

可指数函子之间合成∞-范畴

Exponentiable functors between synthetic $\infty$-categories

本文在合成∞-范畴框架下，利用simplicial同调类型理论，研究并特征化了可指数函子的性质，并验证了结果的语义合理性。

2024-07-25math.ATmath.CT

$(\infty,1)$的综合研究--范畴论：虚构与语义

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

推理弱的高级范畴结构构成了一项具有挑战性的任务，即使是专家。一个主要的原因是集合论的语言在较弱的等价概念下不是不变的，比如同伦等价。从这个角度来看，要求一个更自然地支持这些概念的不同的基础环境是很自然的。我们的工作采取了建议，在原来的文章arXiv：1705.07442由Riehl-Shulman进一步发展合成$(\infty,1)$ -范畴论在单纯同伦型理论，特别是包括研究的cocarrhythmic纤维化。再加上一系列的分析结果，特别是由于里尔-维里蒂和Rasekh，因此，我们的类型理论帐户构成了一个合成理论的纤维化的内部$(\infty,1)$ -类别，w.r.t.通过Shulman关于单叶宇宙严格化的主要结果arXiv：1904.07004，我们得到了任意的Grothendieck-Rezk-Lurie- $(\infty,1)$ -topos。

2022-02-26cs.LOmath.ATmath.CT