Search

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\`ere'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, Comment: 30 pages, submitted to CPP 2023

Convex integration and the holonomic approximation theorem are two well-known pillars of flexibility in differential topology and geometry. They may each seem to have their own flavor and scope. The goal of this paper is to bring some new perspective on this topic. We explain how to prove the holonomic approximation theorem for first order jets using convex integration. More precisely we first prove that this theorem can easily be reduced to proving flexibility of some specific relation. Then we prove this relation is open and ample, hence its flexibility follows from off-the-shelf convex integration., 11 pages

We explain a connection between the algebraic and geometric properties of groups of contact transformations, open book decompositions, and flexible Legendrian embeddings. The main result is that, if a closed contact manifold $(V, \xi)$ has a supporting open book whose pages are flexible Weinstein manifolds, then the connected component $G$ of the identity in its automorphism group is a uniformly simple group: for every non-trivial element $g$, every other element is a product of at most $128(\dim V + 1)$ conjugates of $g^{\pm 1}$. In particular any conjugation invariant norm on this group is bounded. We also prove the later statement still holds for the universal cover of $G$., Comment: 38 pages, 5 figures v2: corrects one silly mistake, updates references and acknowledgments. Submitted version

These notes provide an introduction to Giroux's theory of convex surfaces in contact 3-manifolds and its simplest applications. They put a special emphasis on pictures and discussions of explicit examples. The first goal is to explain why all the information about a contact structure in a neighborhood of a generic surface is encoded by finitely many curves on the surface. Then we describe the bifurcations that happen in generic families of surfaces. As applications, we explain how Giroux used this technology to reprove Bennequin's theorem saying that the standard contact structure on S^3 is tight and Eliashberg's theorem saying that all tight contact structures on S^3 are isotopic to the standard one., 54 pages, 67 figures, based on lectures at the Contact and Symplectic Topology Summer School in Nantes in June 2011

Ozsvath-Szabo contact invariants are a powerful way to prove tightness of contact structures but they are known to vanish in the presence of Giroux torsion. In this paper we construct, on infinitely many manifolds, infinitely many isotopy classes of universally tight torsion free contact structures whose Ozsvath-Szabo invariant vanishes. We also discuss the relation between these invariants and an invariant on T^3 and construct other examples of new phenomena in Heegaard--Floer theory. Along the way, we prove two conjectures of K Honda, W Kazez and G Matic about their contact topological quantum field theory. Almost all the proofs in this paper rely on their gluing theorem for sutured contact invariants., 27 pages, 12 figures