Skip to main content

This month in Mathlib (May 2024)

Source

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 non-degenerate 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 1-dimensional. 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.

  • 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 non-unital 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 Stone-Weierstrass theorem for continuous functions vanishing at zero, namely that the non-unital star subalgebra generated by the identity function is dense. This is essential for PR #13363 which provides uniqueness instances for the non-unital continuous functional calculus. Then PR #13327 and PR #13365 provide instances of the non-unital continuous functional calculus for non-unital 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 non-unital functional calculus by appropriately restricting the unital one to functions vanishing at zero. Finally, PR #13541 obtains a non-unital continuous functional calculus from a unital one, which will be necessary to get a non-unital 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 three-lines 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 non-trivial non-archimedean 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 t-structures 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 3AP-free 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 wrap-around 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 corner-free set and PR #9000 finally proves the Corners theorem and Roth's theorem. They respectively state that a corner-free set in [N] × [N] and a 3AP-free set in [N] have vanishingly small density as N 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 of exp(-(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 finite-product-preserving 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 size-issues, 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.

  • 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 L-functions 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 Fourier-Motzkin 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 tag decl with attribute non_local_attribute.

  • General library maintenance.

    • We are slowly getting rid of Lean 3-inspired 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.
    • As of PR #13271, the notations ∏ x ∈ s, f x and ∑ x ∈ s, f x are global. open scoped BigOperators is now a no-op and downstream projects should stop using it.
    • Since the deprecated attribute now takes an optional since 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 introduced deprecated alias code snippet (PR #13206) to generate @[deprecated (since := "yyyy-mm-dd")] 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 move-decls 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 into RingOfIntegers K : Type _, with the consequence that all typeclass searches on RingOfIntegers K are efficiently indexed on the head (RingOfIntegers) whereas before the head was the very generic CoeSort.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.
    • A sustained effort has started to reduce spurious dependencies between files. There are two lines of work: