论文标题
正式化$ h $ - 原理和球体
Formalising the $h$-principle and sphere eversion
论文作者
论文摘要
在差异拓扑和几何形状中，H原理是某些建筑问题所享有的属性。粗略地说，它指出，解决方案存在的唯一障碍来自代数拓扑。 我们描述了一阶，开放，充足的部分差异关系的本地H原则的形式化。这是差异拓扑结构的重要结果，最初是由格罗莫夫（Gromov）在1973年证明的，这是他全面努力的一部分，它极大地概括了许多以前的灵活性导致拓扑和几何形状。特别是它谴责了Smale著名的Sphere Eversion定理，这是一种视觉上引人注目且违反直觉的结构。我们的形式化利用Theillière从2018年开始实施凸集成。 本文是Sphere Eversion项目的第一部分，旨在将H-Principle的全球版本形式化开放和充足的一阶差异关系，以平滑流形之间的地图。我们目前的向量空间本地版本是此证明的主要成分，足以证明该项目的名义推论。从更广泛的角度来看，该项目的目的是表明，可以以强烈的几何风味形式化高级数学，而不仅可以代数流动。
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière's implementation of convex integration from 2018. This paper is the first part of the sphere eversion project, aiming to formalise the global version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraically-flavoured
