This post summarizes some of the activity that happened in mathlib in October.
- In algebraic geometry, there has been a surge in activity. After the definition of schemes entered mathlib, the development stalled for a while, because the Liquid Tensor Experiment took up a lot of energy and attention. But new contributors showed up, and are pushing the library forward. Two highlights this month include:
In commutative algebra:
In group theory:
- In number theory, PR #9646 and PR #9702 prove that Liouville numbers form a dense $G_δ$ set which has measure zero.
- In combinatorics, PR #7825 proves a generalized version of Hall's marriage theorem using a compactness argument. Using the language of category theory, there is an inverse system of solutions to the marriage problem when restricted to finite subsets of the domain, and the limit of this kind of inverse system is nonempty.
- In measure theory, the series of PRs PR #9462, PR #9461, PR #9576, PR #9679 and PR #9680 prove the Vitali and Besicovitch covering theorems (with the optimal constant for the Besicovitch covering theorem, following Füredi and Loeb, On the best constant for the Besicovitch covering theorem). These theorems ensure that, from a covering of a (not necessarily measurable) set $s$ by nice enough sets (e.g. balls), one can extract a disjoint subfamily covering almost all $s$. They are instrumental in forthcoming results on differentiation of measures.
- In probability:
- In algebraic topology, PR #9252 and PR #9141 set up some basic homotopy theory.
In topological algebra, some foundational parts of the perfectoid project were moved to mathlib after a long time of inactivity:
In differential calculus,
In functional analysis:
- PR #9540 proves the open mapping theorem for maps between affine spaces
- PR #9924 states the Riesz representation theorem uniformly over $ℝ$ and $ℂ$. In 2020, Frédéric Dupuis proved this theorem over both $ℝ$ and $ℂ$ (see PR #4379), but, since mathlib lacked conjugate-linear maps at that time, the $ℂ$-version was stated in a rather awkward way. Conjugate-linear maps were added to mathlib last month and now the $ℝ$ and $ℂ$ versions of the theorem can be stated uniformly.
The core version of Lean was bumped twice in the past month. Most of the changes are in preparation for porting mathlib to Lean 4.