Johan Commelin

I am a postdoc in the group of Stefan Kebekus. My main interest lies in algebraic geometry and algebraic number theory.

From 2017 till 2018 I was a postdoc of Carel Faber in Utrecht (NL). From 2013 till 2017 I was a PhD student in Nijmegen (NL), supervised by Ben Moonen.

Current research topics include: applications of o-minimality to algebraic geometry/topology; in particular, applications of o-minimality to the theory of periods and motives.

News & Olds

My paper (with Rob Y. Lewis) on our formalisation of the ring of Witt vectors has received a Distinguished Paper Award.
My work (with Kevin Buzzard and Patrick Massot) on formalising perfectoid spaces in the Lean theorem prover was recently mentioned in a Quanta article on Lean and its mathematics library mathlib. For more information on mathlib and the community around it, see our community website.
13–17 July 2020, we've had an online workshop on the Lean theorem prover for curious mathematicians: LftCM 2020. It was a great success!

Contact details

@:	`initials` (funny symbol) `math.uni-freiburg.de` (`initials` = `jmc`) — PGP keys: [public] [private]
A:	Room 425 Albert–Ludwigs-Universität Freiburg Mathematisches Institut Ernst-Zermelo-Straße 1 79104 Freiburg im Breisgau Deutschland

Preprints

With Robert Y. Lewis. Formalizing the Ring of Witt Vectors. [arXiv:2010.02595]
With Annette Huber. Exponential periods and o-minimality II. [arXiv:2007.08290]
With Annette Huber and Philipp Habegger. Exponential periods and o-minimality I. [arXiv:2007.08280]
With Victoria Cantoral Farfán. The Mumford–Tate conjecture implies the algebraic Sato–Tate conjecture of Banaszak and Kedlaya [arXiv:1905.04086]

Publications

With Kevin Buzzard and Patrick Massot. Formalising perfectoid spaces Certified Programs and Proofs 2020, 299-312. [offprint] [arXiv:1910.12320] [project webpage]
With Matteo Penegini. On the cohomology of surfaces with p_g = q = 2 and maximal Albanese dimension. Trans. Amer. Math. Soc. 373 (2020) 1749-1773. [arXiv:1901.00193]
On compatibility of the ℓ-adic realisations of an abelian motive. Annales de l’Institut Fourier. Volume 69 (2019) no. 5, p. 2089–2120. [link]
The Mumford–Tate conjecture for products of abelian varieties. Algebraic Geometry (6) 6 (2019) 650–677. [link]
The Mumford–Tate Conjecture for the Product of an Abelian Surface and a K3 Surface. Documenta Math. 21 (2016) 1691–1713. [link]

Current and upcoming teaching

Course	Semester
Teaching: Coxeter Groups and Lie Algebras	Summer 2020
Assistent for Introduction to Algebraic Curves	Summer 2020
Assistent for Mathematics for Natural Scientists II	Summer 2020
Assistent for Cohomology of Algebraic Varieties	Winter 19/20
Assistent for Mathematics for Natural Scientists I	Winter 19/20
Seminar Local Fields	Summer 2019
Linear Algebra 2	Summer 2019

Other writing

My PhD thesis: On ℓ-adic compatibility for abelian motives & the Mumford–Tate conjecture for products of K3 surfaces [Erratum]. Completed in the summer of 2017 under the supervision of Ben Moonen.

I wrote my master's thesis, titled Algebraic cycles, Chow motives, and L-functions, in the spring of 2013 under the supervision of Robin de Jong.

I wrote my bachelor's thesis, titled Tannaka Duality for Finite Groups, in the spring of 2011 under the supervision of Lenny Taelman.

Side projects

Lean and its mathematical library. I am one of the maintainers of the mathematical library of the Lean theorem prover.
Superficie algebriche. (Together with Pieter Belmans.) le superficie algebriche is a tool for studying numerical invariants of minimal algebraic surfaces over the complex numbers. We implemented it in order to better understand the Enriques–Kodaira classification, and to showcase how mathematics can be visualised on the web.
Sloganerator. Together with Pieter Belmans I wrote a web-app that makes it easy to suggest slogans for tags (results) in the Stacks Project.