arXiv subjects

Émile Oleon

Publications and source records attributed to Émile Oleon.

3 recordsLinked to original sources

arXiv2026

Hypercubical manifolds in homotopy type theory

Homotopy type theory provides a logical framework in which geometric constructions and proofs can be carried out synthetically: in this setting, types correspond to spaces up to homotopy, and proofs to homotopy-invariant constructions. Within this context, we introduce a type corresponding to the hypercubical manifold, a space first described by Poincaré in 1895. This manifold is interesting because it offers an approximation of the quaternion group Q, in the sense that it represents the first step toward the construction of a cellular resolution of Q. To validate our definition, we show that it satisfies the expected property: it is the homotopy quotient of the 3-sphere under the natural action of Q. Establishing this result is non-trivial, requiring subtle combinatorial computations based on the flattening lemma, thereby illustrating the constructive power of homotopy type theory. Finally, extending this construction, we introduce higher-dimensional generalizations of the manifold, which provide increasingly precise cellular approximations of Q, and converge toward a delooping of Q.

math.AT↗

arXiv2026

Classifying covering types in homotopy type theory

Covering spaces are a fundamental tool in algebraic topology because of the close relationship they bear with the fundamental groups of spaces. Indeed, they are in correspondence with the subgroups of the fundamental group: this is known as the Galois correspondence. In particular, the covering space corresponding to the trivial group is the universal covering, which is a "1-connected" variant of the original space, in the sense that it has the same homotopy groups, except for the first one which is trivial. In this article, we formalize this correspondence in homotopy type theory, a variant of Martin-Löf type theory in which types can be interpreted as spaces (up to homotopy). Along the way, we develop an n-dimensional generalization of covering spaces. Moreover, in order to demonstrate the applicability of our approach, we formally classify the covering of lens spaces and explain how to construct the Poincaré homology sphere.

cs.LO↗

arXiv2024

Delooping cyclic groups with lens spaces in homotopy type theory

In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called delooping. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to untruncated types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups $\mathbb{Z}_m$ which are cellular, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of lens spaces, which constitute an important family of spaces in algebraic topology. Our definition is based on the computation of an iterative join of suitable maps from the circle to an arbitrary delooping of $\mathbb{Z}_m$. In some sense, this work generalizes the construction of real projective spaces by Buchholtz and Rijke, which handles the case m=2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.

cs.LO↗