A Bézout domain that is not an elementary divisor domain

Abstract

We settle in the negative the longstanding question whether every Bézout domain is an elementary divisor domain by constructing a Bézout domain over which an explicit $2\times 2$ matrix has no Smith normal form. The obstruction is topological and is detected by the Möbius line bundle.

14 pages. Lean formalization available at https://github.com/Zelaron/bezout-counterexample-lean