This month in Mathlib (May 2024)
The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.
There were 667 PRs merged in May 2024.

Algebra
 In Lie theory, Johan Commelin established several important structural properties of Lie algebras. This included PR #12297 which establishes the existence of Cartan subalgebras, PR #13391 which proves that semisimplicity follows from the existence of a nondegenerate invariant form, PR #13265 which specialises this result to the case of the Killing form, and PR #13217 which proves that semisimple Lie algebras have trivial (solvable) radical. Care was taken to ensure that none of these results make any assumptions on the characteristic of the coefficients. Separately, the theory of root spaces was further developed. Firstly PR #12712 added a proof that elements of a Cartan subalgebra are semisimple, and PR #13076 added the definition and basic properties of
sl₂
triples. Using these PR #12937 added the proof that root spaces of a semisimple Lie algebra relative to a splitting Cartan subalgebra are 1dimensional. Andrew Yang then took up the reins and authored a series of PRs culminating in the wonderful PR #13307 which proved that the roots of a semisimple Lie algebra are an abstract (reduced, crystallographic) root system.  Amelia Livingston added some boilerplate defining coalgebra isomorphisms in PR #11970, the category of coalgebras in PR #11972, and homomorphisms and isomorphisms of bialgebras in PR #11962 and PR #11971. This API will be used to define the monoidal category structure on co/bi/Hopf algebras. It will also be linked to Kim Morrison's work on co/bi/Hopf monoids, as well as the material about group objects formalised at Formalisation of Mathematics: Workshop for Women and Mathematicians of Minority Gender with Rebecca Bellovin and Sophie Morel.
 Mitchell Lee laid the groundwork for future material on Coxeter groups. PR #11465 defines the length function on a Coxeter group and proves its basic properties. PR #11466 defines reflections and inversions in a Coxeter group and proves that the inversion sequence of a reduced word consists of distinct reflections.
 In PR #12647, Mitchell Lee formalized a proof of the equational criterion for vanishing, a necessary and sufficient criterion for a sum of pure tensors in the tensor product of two modules to vanish.
 Scott Carnahan is working on defining vertex algebras: PR #11797 defines heterogeneous vertex operators.
 In Lie theory, Johan Commelin established several important structural properties of Lie algebras. This included PR #12297 which establishes the existence of Cartan subalgebras, PR #13391 which proves that semisimplicity follows from the existence of a nondegenerate invariant form, PR #13265 which specialises this result to the case of the Killing form, and PR #13217 which proves that semisimple Lie algebras have trivial (solvable) radical. Care was taken to ensure that none of these results make any assumptions on the characteristic of the coefficients. Separately, the theory of root spaces was further developed. Firstly PR #12712 added a proof that elements of a Cartan subalgebra are semisimple, and PR #13076 added the definition and basic properties of

Algebraic Geometry.
 PR #12917 by Jonas van der Schaaf, Amelia Livingston and later Christian Merten defines closed immersions.

Analysis.
 Jireh Loreaux and Anatole Dedecker completed the development of the nonunital continuous functional calculus. Although the generic API has been in place for a few months, the relevant instances for C⋆algebras were missing. Work progressed in a piecemeal fashion, but PR #13326 provides a version of the StoneWeierstrass theorem for continuous functions vanishing at zero, namely that the nonunital star subalgebra generated by the identity function is dense. This is essential for PR #13363 which provides uniqueness instances for the nonunital continuous functional calculus. Then PR #13327 and PR #13365 provide instances of the nonunital continuous functional calculus for nonunital C⋆algebras and generic restriction lemmas for scalar subrings. These are obtained by first considering the unitization of the algebra, obtaining a unital functional calculus there, and then realizing a nonunital functional calculus by appropriately restricting the unital one to functions vanishing at zero. Finally, PR #13541 obtains a nonunital continuous functional calculus from a unital one, which will be necessary to get a nonunital instance on matrices, for example.
 Sébastien Gouëzel completed the proof that the Fourier transform is well defined on the Schwartz space of a Euclidean space. PR #12769 shows how one can bound derivatives of the Fourier transform of a function (multiplied by a power function) in terms of derivatives of the initial function (multiplied by a power function) and PR #11937 proves a version of integration by parts for line/Fréchet derivatives. PR #12144 puts these results together to define the Fourier transform as a continuous linear equivalence on Schwartz space (taking advantage of the Fourier inversion formula to get the inverse direction from the forward direction). Note that the Schwartz space is a Fréchet space but not a normed space, so this builds on a lot of analysis on Fréchet spaces in terms of families of seminorms.
 Chris Birkbeck proved that Eisenstein series converge uniformly in PR #10377 and that they are holomorphic in PR #11013. This will soon be used to show that they are modular forms.
 Xavier Généreux proved the Hadamard threelines theorem in the special case of the unit vertical strip in PR #7919. This will be used to interpolate norms.
 In PR #12669, Mitchell Lee proved that the completion of a nonarchimedean group is again nonarchimedean.
 In PR #12432, it is shown that nontrivial nonarchimedean norms correspond to rank 1 valuations.

Category Theory.
 After an important effort by Joël Riou, derived categories of abelian categories and their triangulated structure are now in Mathlib since PR #11806. Using the triangulated structure on the homotopy category of an abelian categories (which was already obtained during the Liquid Tensor Experiment), this essentially follows from the localization theorem for triangulated categories PR #11786. Derived categories shall soon have more applications inside mathlib, thanks to the formalization of total derived functors PR #12788 and tstructures PR #12619.
 We set up some of the basic theory of comonoid objects in monoidal categories, laying the foundation for work on bimonoids and Hopf monoids (and eventually group schemes, etc). The definition was in PR #10091, and the fact that oplax monoidal functors (newly defined in PR #12856) take comonoids to comonoids in PR #12858. In a braided category, the comonoid objects themselves have a monoidal category structure, developed in PR #10098. Finally, in a cartesian monoidal category, comonoids are not interesting: every object is a comonoid object in a unique way, using the diagonal map as the comultiplication. This is proved in PR #10103.

Combinatorics.

Thanks to the reviews by Thomas Bloom, a long sequence of three years old material by Yaël Dillies and Bhavik Mehta culminating in Roth's theorem on arithmetic progressions was finally merged:
 PR #12526 defines locally linear graphs, PR #12570 constructs such graphs from a set of specified triangles respecting some conditions, PR #12523 uses that construction to deduce the Triangle removal lemma from the Regularity lemma.
 PR #12701 redefines sets without arithmetic progressions of length 3 (aka 3APfree sets) so that they behave correctly in characteristic two. PR #12546 refactors Freiman homomorphisms and isomorphisms from a bundled design to unbundled predicates. This makes them much easier to use. PR #12551 then proves the no wraparound principle stating that additive structure in sets is independent of the ambient group so long as torsion is much bigger than the diameter of the sets.
 Building up on thoses two series of PRs, PR #13074 defines corners and cornerfree set and PR #9000 finally proves the Corners theorem and Roth's theorem. They respectively state that a cornerfree set in
[N] × [N]
and a 3APfree set in[N]
have vanishingly small density asN
goes to infinity.
APAP already contains the stronger result that the density goes to zero as
1/log log N
, and will soon prove the state of the art bound ofexp((log N)^1/9)
. 
PR #10555 defines dissociation of sets, a sort of "local" version of linear independence obtained by restricting the scalars to
{1, 0, 1}
. This will soon be used to prove important results in additive combinatorics.  Mathlib finally knows about Hamiltonian paths and cycles thanks to a team effort started at Lean for the Curious Mathematician 2023 in Düsseldorf by Rishi Mehta and Linus Sommer under the supervision of Bhavik Mehta, and recently continued by Lode Vermeulen in PR #7102.


Condensed mathematics.
 The work towards getting the basics of condensed mathematics into Mathlib started about a year ago at a workshop in Copenhagen organized by Dagur Asgeirsson. The participants made great progress and proved results like the characterization of condensed sets as finiteproductpreserving presheaves on
Stonean
. Since then, Dagur has been moving the material to Mathlib and developing it further. This month landed: PR #11586 defining light condensed objects. This is a concept introduced by Clausen and Scholze less than a year ago, and is an improvement over condensed sets in that it removes certain sizeissues, as it is a sheaf over an essentially small site.
 PR #12870 proving the explicit sheaf condition for condensed objects in a very general target category. Previously, we only had this in certain concrete categories.
 PR #9513 constructing colimits of light profinite objects.
 PR #11585 proving that the category of light profinite objects is precoherent.
 The work towards getting the basics of condensed mathematics into Mathlib started about a year ago at a workshop in Copenhagen organized by Dagur Asgeirsson. The participants made great progress and proved results like the characterization of condensed sets as finiteproductpreserving presheaves on

Number Theory.
 PR #12897 defines the Hurwitz zeta function, and proves its key properties (analytic continuation + functional equation). This is a generalisation of the Riemann zeta function, and is an important step towards Dirichlet Lfunctions in the near future. (Subsidiary PR's include PR #12779, PR #12265, PR #13347, PR #13273.)

Order Theory.
 Stone duality between the categories of Boolean algebras and of profinite spaces is slowly moving from the StoneDualityInLean project: PR #12705 proves that a disjoint filter and ideal in a bounded distributive lattice can always be separated by a prime ideal.
 Christopher Hoskin continues introducing topologies relevant to order theory: PR #11710 defines the Lawson Topology.

Metaprogramming.
 Miyahara Kō heroically ported the
cc
tactic to Lean 4: PR #11956, PR #11960 and PR #5938.  Damiano Testa and Yaël Dillies replaced the
mk_all
shell script hardcoded to Mathlib with a Lean script that dynamically figures out the Lean libraries (sadly, Mathlib still needs some separate handling) in PR #11853, and PR #11874 made use of it in the "Check all files are imported" CI step. The script can now be used by any project downstream of Mathlib. If you maintain such a project, we encourage you to switch over to the new script and report eventual bugs.  Vasily Nesterov implemented a simplex algorithm oracle in PR #12014. This is now the default oracle for
linarith
instead of the much slower FourierMotzkin oracle. 
PR #13190 and PR #13293 by Michael Rothgang and Damiano Testa neuters a very pernicious footgun: Contrary to expectations,
attribute [non_local_attribute] decl in
would globally tagdecl
with attributenon_local_attribute
.
 Miyahara Kō heroically ported the

General library maintenance.
 We are slowly getting rid of Lean 3inspired syntax in Mathlib. New uses will soon be linted against in Mathlib and we encourage downstream projects to follow suit and adopt the new syntax.

refine'
is a tactic that mimics the Lean 3 behavior ofrefine
, mostly useful when porting Lean 3 code. It was decided to avoid using it in favor of the more declarativerefine
, or ofapply
in the rare cases whererefine
handles metavariables suboptimally. The following PRs started replacingrefine'
withrefine
orapply
: PR #12755, PR #12851, PR #12997, PR #13059, PR #13062, PR #13166, PR #13234, PR #13287, PR #13357, PR #13383, PR #13472, PR #13474, PR #13490, PR #13385.  "Streamofconsciousness
obtain
" is now deprecated. PR #12850 and PR #13219 removed all occurrences of this syntax in Mathlib.

 As of PR #13271, the notations
∏ x ∈ s, f x
and∑ x ∈ s, f x
are global.open scoped BigOperators
is now a noop and downstream projects should stop using it.  Since the
deprecated
attribute now takes an optionalsince
field, we are systematising its use so that we can later programmatically remove all deprecations older than N months. The following PRs added dates to existing deprecations: PR #12407, PR #12547, PR #12947, PR #12408, PR #12597, PR #13185, PR #13182, PR #12598, PR #13188, PR #13368. Note that within Mathlib you can use the newly introduceddeprecated alias
code snippet (PR #13206) to generate@[deprecated (since := "yyyymmdd")] old_name := new_name
.  To help reviewing large PRs, especially refactors, a bot now posts a diff of declaration names. This was introduced as a CI step in PR #12515 whose output is available as a comment when tagging a PR with the new
movedecls
label (see PR #12844).  Several performance improvements were made. Here are two that deserve to be known more widely:
 It was discovered that defining concrete types as subobjects can be a cause of poor performance. For example, PR #12386 turns
ringOfIntegers K : Subalgebra ℤ K
intoRingOfIntegers K : Type _
, with the consequence that all typeclass searches onRingOfIntegers K
are efficiently indexed on the head (RingOfIntegers
) whereas before the head was the very genericCoeSort.coe
.  In a similar fashion, some simp lemmas accidentally had a lambda on their LHS, meaning that their key in simp's discrimination tree was maximally general and that simp would try rewriting with them in every location. Some such lemmas were unsimped in PR #13164.
 It was discovered that defining concrete types as subobjects can be a cause of poor performance. For example, PR #12386 turns
 A sustained effort has started to reduce spurious dependencies between files. There are two lines of work:
 Reducing the long pole: Assuming Mathlib is built on an infinitely parallelizing machine, there is some sequence of files, each importing the previous, that takes the longest to build. We call this sequence the "long pole". As it is a cap on performance, it is natural to try shortening it. After PR #12777, PR #12401, the long pole has left the
RingTheory
folder entirely.  Reducing imports to basic files: The theory of basic algebra, order theory and data structures feed into each other at various points. For example, we need to know some order properties of addition and multiplication on
Nat
andInt
to talk about powers in a group, and we need finite sets to define finite sums and finite suprema/infima. It is overwhelmingly easy to create an almostcircular import graph ricocheting between those three areas. TheNat
 andInt
specific lemmas in Core and Batteries are an opportunity to cut the knot: These lemmas do not depend on Mathlib's algebraic order hierarchy, hence can be used in basic algebra and data structures without overimporting. The following PRs are steps towards that: PR #11986, PR #12710, PR #12828, PR #12736, PR #12825, PR #12817, PR #12823, PR #12872, PR #12829, PR #12862, PR #12835, PR #12821, PR #12818, PR #12836, PR #12832, PR #12882, PR #12975, PR #11855, PR #13029, PR #12985, PR #13008, PR #13033, PR #12845, PR #12974, PR #11863, PR #12959, PR #13030, PR #13031, PR #13005, PR #13140, PR #13139, PR #12990, PR #13184, PR #13197, PR #13138, PR #12957, PR #13222, PR #13224, PR #13242, PR #13288, PR #13003, PR #13205, PR #13289, PR #13244, PR #13305, PR #13274, PR #13253, PR #13268, PR #13147, PR #13243.
 Reducing the long pole: Assuming Mathlib is built on an infinitely parallelizing machine, there is some sequence of files, each importing the previous, that takes the longest to build. We call this sequence the "long pole". As it is a cap on performance, it is natural to try shortening it. After PR #12777, PR #12401, the long pole has left the
 We are slowly getting rid of Lean 3inspired syntax in Mathlib. New uses will soon be linted against in Mathlib and we encourage downstream projects to follow suit and adopt the new syntax.