Papers With

← All papers
First page of Finite Chains of Two-Complexes and Acyclic Covers

Finite Chains of Two-Complexes and Acyclic Covers

Laurent Bartholdi, Roman Mikhailov

math.GT Oct 7, 2026 · v1 math.GR
formalization mathlib topology
Read PDF arXiv abstract
TL;DR
Theorem A, characterizing two-complexes with finite chains zero on π2 via acyclic covers, was formalized in Lean/Mathlib, with the formalization slated for the Palomar repository.
Abstract
A negative answer to Whitehead's asphericity problem would follow from an infinite chain of two-complexes, starting with a non-aspherical one, in which every inclusion induces the zero map on second homotopy groups. We prove that a connected two-complex $K$ is the first term of such chains of every finite length if and only if $K$ has a connected acyclic regular cover. In particular, there is a finite non-aspherical two-complex $K$, a presentation complex of $\mathrm{SL}(2,5)$, such that for every $n$ there is a strictly increasing chain of finite two-complexes $K=K_0\subset K_1\subset\dots\subset K_n$ in which all inclusions are zero on $π_2$.
Problem

A negative answer to Whitehead's asphericity problem would follow from an infinite chain of two-complexes, starting with a non-aspherical one, in which every inclusion is zero on π2. The paper asks which two-complexes start such chains of every finite length.

Approach

The authors prove that a connected two-complex K starts strictly increasing chains of every finite length with all inclusions zero on π2 if and only if K has a connected acyclic regular cover. The necessity direction uses cycle tests and a Strebel-type injectivity lemma. Sufficiency builds chains over the acyclic cover from presentations and blocks derived from Davis's moment-angle cube complexes and relative hyperbolization. A descent pushout argument then transfers these chains to K. Theorem A was formalized in Lean/Mathlib.

Results

Theorem A gives the equivalence, with finite complexes when K is finite and acyclic. As a corollary, a presentation complex of SL(2,5) with π2 ≅ Z^119 begins finite chains of every length in which all inclusions are zero on π2.