7 papers
Model categories for o-minimal geometry
Reid Barton, Johan Commelin
We introduce a model category of spaces based on the definable sets of an o-minimal expansion of a real closed field. As a model category, it resembles the category of topological…
Formalizing the Ring of Witt Vectors
Johan Commelin, Robert Y. Lewis
The ring of Witt vectors over a base ring is an important tool in algebraic number theory and lies at the foundations of modern -adic Hodge theory. $\mathbb{W…
Formalising perfectoid spaces
Kevin Buzzard, Johan Commelin, Patrick Massot
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geome…
The Mumford-Tate conjecture implies the algebraic Sato-Tate conjecture of Banaszak and Kedlaya
Victoria Cantoral Farfán, Johan Commelin
The algebraic Sato-Tate conjecture was initially introduced by Serre and then discussed by Banaszak and Kedlaya. This note shows that the Mumford-Tate conjecture for an abelian var…
On the cohomology of surfaces with and maximal Albanese dimension
Johan Commelin, Matteo Penegini
In this paper we study the cohomology of smooth projective complex surfaces of general type with invariants and surjective Albanese morphism. We show that on a Ho…
The Mumford--Tate conjecture for products of abelian varieties
Johan Commelin
Let be a smooth projective variety over a finitely generated field of characteristic~ and fix an embedding . The Mumford--Tate conjecture is a prec…