Showing cs.LOShow all
2 papers · 1 filter
cs.LO2020
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…
cs.LO2019
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…