From 3a4ca49069f0129ff397a741f7796d2ea0ce5e89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 1 Jul 2024 14:40:13 +0200 Subject: [PATCH] Month in Mathlib May 2024 - Fixes (#78) Indentation was wrong, some links were dead and a PR shouldn't have been mentioned. --- posts/month-in-mathlib-may-2024.md | 106 ++++++++++++++--------------- 1 file changed, 53 insertions(+), 53 deletions(-) diff --git a/posts/month-in-mathlib-may-2024.md b/posts/month-in-mathlib-may-2024.md index 09fee094..52b1eb25 100644 --- a/posts/month-in-mathlib-may-2024.md +++ b/posts/month-in-mathlib-may-2024.md @@ -1,7 +1,7 @@ --- author: 'Mathlib community' category: 'month-in-mathlib' -date: 2024-06-11 22:00:56+00:00 +date: 2024-07-01 12:00:00+00:00 description: '' has_math: true link: '' @@ -18,72 +18,72 @@ 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](https://github.com/leanprover-community/mathlib4/pull/12297) which establishes the existence of Cartan subalgebras, [PR #13391](https://github.com/leanprover-community/mathlib4/pull/13391) which proves that semisimplicity follows from the existence of a non-degenerate invariant form, [PR #13265](https://github.com/leanprover-community/mathlib4/pull/13265) which specialises this result to the case of the Killing form, and [PR #13217](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12712) added a proof that elements of a Cartan subalgebra are semisimple, and [PR #13076](https://github.com/leanprover-community/mathlib4/pull/13076) added the definition and basic properties of `sl₂` triples. Using these [PR #12937](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/13307) which proved that the roots of a semisimple Lie algebra are an abstract (reduced, crystallographic) root system. - * [PR #12721](https://github.com/leanprover-community/mathlib4/pull/12721) :: feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian - * Amelia Livingston added some boilerplate defining coalgebra isomorphisms in [PR #11970](https://github.com/leanprover-community/mathlib4/pull/11970), the category of coalgebras in [PR #11972](https://github.com/leanprover-community/mathlib4/pull/11972), and homomorphisms and isomorphisms of bialgebras in [PR #11962](https://github.com/leanprover-community/mathlib4/pull/11962) and [PR #11971](https://github.com/leanprover-community/mathlib4/pull/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](https://www.icms.org.uk/Formalisation) 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](https://github.com/leanprover-community/mathlib4/pull/11797) defines heterogeneous vertex operators. + * In Lie theory, Johan Commelin established several important structural properties of Lie algebras. This included [PR #12297](https://github.com/leanprover-community/mathlib4/pull/12297) which establishes the existence of Cartan subalgebras, [PR #13391](https://github.com/leanprover-community/mathlib4/pull/13391) which proves that semisimplicity follows from the existence of a non-degenerate invariant form, [PR #13265](https://github.com/leanprover-community/mathlib4/pull/13265) which specialises this result to the case of the Killing form, and [PR #13217](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12712) added a proof that elements of a Cartan subalgebra are semisimple, and [PR #13076](https://github.com/leanprover-community/mathlib4/pull/13076) added the definition and basic properties of `sl₂` triples. Using these [PR #12937](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11970), the category of coalgebras in [PR #11972](https://github.com/leanprover-community/mathlib4/pull/11972), and homomorphisms and isomorphisms of bialgebras in [PR #11962](https://github.com/leanprover-community/mathlib4/pull/11962) and [PR #11971](https://github.com/leanprover-community/mathlib4/pull/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](https://www.icms.org.uk/Formalisation) with Rebecca Bellovin and Sophie Morel. + * Mitchell Lee laid the groundwork for future material on Coxeter groups. [PR #11465](https://github.com/leanprover-community/mathlib4/pull/11465) defines the length function on a Coxeter group and proves its basic properties. [PR #11466](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11797) defines heterogeneous vertex operators. * Algebraic Geometry. - * [PR #12917](https://github.com/leanprover-community/mathlib4/pull/12917) by Jonas van der Schaaf, Amelia Livingston and later Christian Merten defines closed immersions. + * [PR #12917](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/13326) provides a version of the Stone-Weiertrass 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](https://github.com/leanprover-community/mathlib4/pull/13363) which provides uniqueness instances for the non-unital continuous functional calculus. Then [PR #13327](https://github.com/leanprover-community/mathlib4/pull/13327) and [PR #13365](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11937) proves a version of integration by parts for line/Fréchet derivatives. [PR #12144](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/10377) and that they are holomorphic in [PR #11013](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12432), it is shown that non-trivial non-archimedean norms correspond to rank 1 valuations. + * 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](https://github.com/leanprover-community/mathlib4/pull/13326) provides a version of the Stone-Weiertrass 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](https://github.com/leanprover-community/mathlib4/pull/13363) which provides uniqueness instances for the non-unital continuous functional calculus. Then [PR #13327](https://github.com/leanprover-community/mathlib4/pull/13327) and [PR #13365](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11937) proves a version of integration by parts for line/Fréchet derivatives. [PR #12144](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/10377) and that they are holomorphic in [PR #11013](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/7919). This will be used to interpolate norms. + * In [PR #12669](https://github.com/leanprover-community/mathlib4/pull/12669), Mitchell Lee proved that the completion of a nonarchimedean group is again nonarchimedean. + * In [PR #12432](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11806). Using the triangulated structure on the homotopy category of an abelian categories (which was already obtained during the [Liquid Tensor Experiment](https://leanprover-community.github.io/blog/posts/lte-final/)), this essentially follows from the localization theorem for triangulated categories [PR #11786](https://github.com/leanprover-community/mathlib4/pull/11786). Derived categories shall soon have more applications inside mathlib, thanks to the formalization of total derived functors [PR #12788](https://github.com/leanprover-community/mathlib4/pull/12788) and t-structures [PR #12619](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/10091), and the fact that oplax monoidal functors (newly defined in [PR #12856](https://github.com/leanprover-community/mathlib4/pull/12856)) - take comonoids to comonoids in - [PR #12858](https://github.com/leanprover-community/mathlib4/pull/12858). In a braided category, the comonoid objects themselves have a monoidal category structure, - developed in [PR #10098](https://github.com/leanprover-community/mathlib4/pull/10098). Finally, in a cartesion 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](https://github.com/leanprover-community/mathlib4/pull/10103). + * After an important effort by Joël Riou, derived categories of abelian categories and their triangulated structure are now in Mathlib since [PR #11806](https://github.com/leanprover-community/mathlib4/pull/11806). Using the triangulated structure on the homotopy category of an abelian categories (which was already obtained during the [Liquid Tensor Experiment](https://leanprover-community.github.io/blog/posts/lte-final/)), this essentially follows from the localization theorem for triangulated categories [PR #11786](https://github.com/leanprover-community/mathlib4/pull/11786). Derived categories shall soon have more applications inside mathlib, thanks to the formalization of total derived functors [PR #12788](https://github.com/leanprover-community/mathlib4/pull/12788) and t-structures [PR #12619](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/10091), and the fact that oplax monoidal functors (newly defined in [PR #12856](https://github.com/leanprover-community/mathlib4/pull/12856)) + take comonoids to comonoids in + [PR #12858](https://github.com/leanprover-community/mathlib4/pull/12858). In a braided category, the comonoid objects themselves have a monoidal category structure, + developed in [PR #10098](https://github.com/leanprover-community/mathlib4/pull/10098). Finally, in a cartesion 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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12526) defines locally linear graphs, [PR #12570](https://github.com/leanprover-community/mathlib4/pull/12570) constructs such graphs from a set of specified triangles respecting some conditions, [PR #12523](https://github.com/leanprover-community/mathlib4/pull/12523) uses that construction to deduce the Triangle removal lemma from the Regularity lemma. - * [PR #12701](https://github.com/leanprover-community/mathlib4/pull/12701) redefines sets without arithmetic progressions of length 3 (aka 3AP-free sets) so that they behave correctly in characteristic two. [PR #12546](https://github.com/leanprover-community/mathlib4/pull/12546) refactors Freiman homomorphisms and isomorphisms from a bundled design to unbundled predicates. This makes them much easier to use. [PR #12551](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/13074) defines corners and corner-free set and [PR #9000](https://github.com/leanprover-community/mathlib4/pull/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. +* 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](https://github.com/leanprover-community/mathlib4/pull/12526) defines locally linear graphs, [PR #12570](https://github.com/leanprover-community/mathlib4/pull/12570) constructs such graphs from a set of specified triangles respecting some conditions, [PR #12523](https://github.com/leanprover-community/mathlib4/pull/12523) uses that construction to deduce the Triangle removal lemma from the Regularity lemma. + * [PR #12701](https://github.com/leanprover-community/mathlib4/pull/12701) redefines sets without arithmetic progressions of length 3 (aka 3AP-free sets) so that they behave correctly in characteristic two. [PR #12546](https://github.com/leanprover-community/mathlib4/pull/12546) refactors Freiman homomorphisms and isomorphisms from a bundled design to unbundled predicates. This makes them much easier to use. [PR #12551](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/13074) defines corners and corner-free set and [PR #9000](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/YaelDillies/LeanAPAP) 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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/7102). + [APAP](https://github.com/YaelDillies/LeanAPAP) 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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/9513) constructing colimits of light profinite objects. - * [PR #11585](https://github.com/leanprover-community/mathlib4/pull/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 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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/9513) constructing colimits of light profinite objects. + * [PR #11585](https://github.com/leanprover-community/mathlib4/pull/11585) proving that the category of light profinite objects is precoherent. + * Number Theory. - * [PR #12897](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12779), [PR #12265](https://github.com/leanprover-community/mathlib4/pull/12265), [PR #13347](https://github.com/leanprover-community/mathlib4/pull/13347), [PR #13273](https://github.com/leanprover-community/mathlib4/pull/13273).) + * [PR #12897](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12779), [PR #12265](https://github.com/leanprover-community/mathlib4/pull/12265), [PR #13347](https://github.com/leanprover-community/mathlib4/pull/13347), [PR #13273](https://github.com/leanprover-community/mathlib4/pull/13273).) * Order Theory. - * Stone duality between the categories of Boolean algebras and of profinite spaces is slowly moving from the [StoneDualityInLean project](https://github.com/samvang/StoneDualityInLean/): [PR #12705](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11710) defines the Lawson Topology. + * Stone duality between the categories of Boolean algebras and of profinite spaces is slowly moving from the [StoneDualityInLean project](https://github.com/samvang/StoneDualityInLean/): [PR #12705](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11710) defines the Lawson Topology. * Metaprogramming. - * Miyahara Kō heroically ported the `cc` tactic to Lean 4: [PR #11956](https://github.com/leanprover-community/mathlib4/pull/11956), [PR #11960](https://github.com/leanprover-community/mathlib4/pull/11960) and [PR #5938](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11853), and [PR #11874](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12014). This is now the default oracle for `linarith` instead of the much slower Fourier-Motzkin oracle. - * [PR #13190](https://github.com/leanprover-community/mathlib4/pull/13190) and [PR #13293](https://github.com/leanprover-community/mathlib4/pull/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`. + * Miyahara Kō heroically ported the `cc` tactic to Lean 4: [PR #11956](https://github.com/leanprover-community/mathlib4/pull/11956), [PR #11960](https://github.com/leanprover-community/mathlib4/pull/11960) and [PR #5938](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/11853), and [PR #11874](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12014). This is now the default oracle for `linarith` instead of the much slower Fourier-Motzkin oracle. + * [PR #13190](https://github.com/leanprover-community/mathlib4/pull/13190) and [PR #13293](https://github.com/leanprover-community/mathlib4/pull/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 maintainance. - * 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. - * `refine'` is a tactic that mimics the Lean 3 behavior of `refine`, mostly useful when porting Lean 3 code. It was decided to avoid using it in favor of the more declarative `refine`, or of `apply` in the rare cases where `refine` handles metavariables suboptimally. The following PRs started replacing `refine'` with `refine` or `apply`: [PR #12755](https://github.com/leanprover-community/mathlib4/pull/12755), [PR #12851](https://github.com/leanprover-community/mathlib4/pull/12851), [PR #12997](https://github.com/leanprover-community/mathlib4/pull/12997), [PR #13059](https://github.com/leanprover-community/mathlib4/pull/13059), [PR #13062](https://github.com/leanprover-community/mathlib4/pull/13062), [PR #13166](https://github.com/leanprover-community/mathlib4/pull/13166), [PR #13234](https://github.com/leanprover-community/mathlib4/pull/13234), [PR #13287](https://github.com/leanprover-community/mathlib4/pull/13287), [PR #13357](https://github.com/leanprover-community/mathlib4/pull/13357), [PR #13383](https://github.com/leanprover-community/mathlib4/pull/13383), [PR #13472](https://github.com/leanprover-community/mathlib4/pull/13472), [PR #13474](https://github.com/leanprover-community/mathlib4/pull/13474), [PR #13490](https://github.com/leanprover-community/mathlib4/pull/13490), [PR #13385](https://github.com/leanprover-community/mathlib4/pull/13385). - * "Stream-of-consciousness `obtain`" is now deprecated. [PR #12850](https://github.com/leanprover-community/mathlib4/pull/12850) and [PR #13219](https://github.com/leanprover-community/mathlib4/pull/13219) removed all occurrences of this syntax in Mathlib. - * As of [PR #13271](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12407), [PR #12547](https://github.com/leanprover-community/mathlib4/pull/12547), [PR #12947](https://github.com/leanprover-community/mathlib4/pull/12947), [PR #12408](https://github.com/leanprover-community/mathlib4/pull/12408), [PR #12597](https://github.com/leanprover-community/mathlib4/pull/12597), [PR #13185](https://github.com/leanprover-community/mathlib4/pull/13185), [PR #13182](https://github.com/leanprover-community/mathlib4/pull/13182), [PR #12598](https://github.com/leanprover-community/mathlib4/pull/12598), [PR #13188](https://github.com/leanprover-community/mathlib4/pull/13188), [PR #13368](https://github.com/leanprover-community/mathlib4/pull/13368). Note that within Mathlib you can use the newly introduced `deprecated alias` code snippet ([PR #13206](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12515) whose output is available as a comment when tagging a PR with the new `move-decls` label (see [PR #12844](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/13164). - * 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](https://github.com/leanprover-community/mathlib4/pull/12777), [PR #12401](https://github.com/leanprover-community/mathlib4/pull/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` and `Int` 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 almost-circular import graph ricocheting between those three areas. The `Nat`- and `Int`-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 over-importing. The following PRs are steps towards that: [PR #11986](https://github.com/leanprover-community/mathlib4/pull/11986), [PR #12710](https://github.com/leanprover-community/mathlib4/pull/12710), [PR #12828](https://github.com/leanprover-community/mathlib4/pull/12828), [PR #12736](https://github.com/leanprover-community/mathlib4/pull/12736), [PR #12825](https://github.com/leanprover-community/mathlib4/pull/12825), [PR #12817](https://github.com/leanprover-community/mathlib4/pull/12817), [PR #12823](https://github.com/leanprover-community/mathlib4/pull/12823), [PR #12872](https://github.com/leanprover-community/mathlib4/pull/12872), [PR #12829](https://github.com/leanprover-community/mathlib4/pull/12829), [PR #12862](https://github.com/leanprover-community/mathlib4/pull/12862), [PR #12835](https://github.com/leanprover-community/mathlib4/pull/12835), [PR #12821](https://github.com/leanprover-community/mathlib4/pull/12821), [PR #12818](https://github.com/leanprover-community/mathlib4/pull/12818), [PR #12836](https://github.com/leanprover-community/mathlib4/pull/12836), [PR #12832](https://github.com/leanprover-community/mathlib4/pull/12832), [PR #12882](https://github.com/leanprover-community/mathlib4/pull/12882), [PR #12975](https://github.com/leanprover-community/mathlib4/pull/12975), [PR #11855](https://github.com/leanprover-community/mathlib4/pull/11855), [PR #13029](https://github.com/leanprover-community/mathlib4/pull/13029), [PR #12985](https://github.com/leanprover-community/mathlib4/pull/12985), [PR #13008](https://github.com/leanprover-community/mathlib4/pull/13008), [PR #13033](https://github.com/leanprover-community/mathlib4/pull/13033), [PR #12845](https://github.com/leanprover-community/mathlib4/pull/12845), [PR #12974](https://github.com/leanprover-community/mathlib4/pull/12974), [PR #11863](https://github.com/leanprover-community/mathlib4/pull/11863), [PR #12959](https://github.com/leanprover-community/mathlib4/pull/12959), [PR #13030](https://github.com/leanprover-community/mathlib4/pull/13030), [PR #13031](https://github.com/leanprover-community/mathlib4/pull/13031), [PR #13005](https://github.com/leanprover-community/mathlib4/pull/13005), [PR #13140](https://github.com/leanprover-community/mathlib4/pull/13140), [PR #13139](https://github.com/leanprover-community/mathlib4/pull/13139), [PR #12990](https://github.com/leanprover-community/mathlib4/pull/12990), [PR #13184](https://github.com/leanprover-community/mathlib4/pull/13184), [PR #13197](https://github.com/leanprover-community/mathlib4/pull/13197), [PR #13138](https://github.com/leanprover-community/mathlib4/pull/13138), [PR #12957](https://github.com/leanprover-community/mathlib4/pull/12957), [PR #13222](https://github.com/leanprover-community/mathlib4/pull/13222), [PR #13224](https://github.com/leanprover-community/mathlib4/pull/13224), [PR #13242](https://github.com/leanprover-community/mathlib4/pull/13242), [PR #13288](https://github.com/leanprover-community/mathlib4/pull/13288), [PR #13003](https://github.com/leanprover-community/mathlib4/pull/13003), [PR #13205](https://github.com/leanprover-community/mathlib4/pull/13205), [PR #13289](https://github.com/leanprover-community/mathlib4/pull/13289), [PR #13244](https://github.com/leanprover-community/mathlib4/pull/13244), [PR #13305](https://github.com/leanprover-community/mathlib4/pull/13305), [PR #13274](https://github.com/leanprover-community/mathlib4/pull/13274), [PR #13253](https://github.com/leanprover-community/mathlib4/pull/13253), [PR #13268](https://github.com/leanprover-community/mathlib4/pull/13268), [PR #13147](https://github.com/leanprover-community/mathlib4/pull/13147), [PR #13243](https://github.com/leanprover-community/mathlib4/pull/13243). \ No newline at end of file + * 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. + * `refine'` is a tactic that mimics the Lean 3 behavior of `refine`, mostly useful when porting Lean 3 code. It was decided to avoid using it in favor of the more declarative `refine`, or of `apply` in the rare cases where `refine` handles metavariables suboptimally. The following PRs started replacing `refine'` with `refine` or `apply`: [PR #12755](https://github.com/leanprover-community/mathlib4/pull/12755), [PR #12851](https://github.com/leanprover-community/mathlib4/pull/12851), [PR #12997](https://github.com/leanprover-community/mathlib4/pull/12997), [PR #13059](https://github.com/leanprover-community/mathlib4/pull/13059), [PR #13062](https://github.com/leanprover-community/mathlib4/pull/13062), [PR #13166](https://github.com/leanprover-community/mathlib4/pull/13166), [PR #13234](https://github.com/leanprover-community/mathlib4/pull/13234), [PR #13287](https://github.com/leanprover-community/mathlib4/pull/13287), [PR #13357](https://github.com/leanprover-community/mathlib4/pull/13357), [PR #13383](https://github.com/leanprover-community/mathlib4/pull/13383), [PR #13472](https://github.com/leanprover-community/mathlib4/pull/13472), [PR #13474](https://github.com/leanprover-community/mathlib4/pull/13474), [PR #13490](https://github.com/leanprover-community/mathlib4/pull/13490), [PR #13385](https://github.com/leanprover-community/mathlib4/pull/13385). + * "Stream-of-consciousness `obtain`" is now deprecated. [PR #12850](https://github.com/leanprover-community/mathlib4/pull/12850) and [PR #13219](https://github.com/leanprover-community/mathlib4/pull/13219) removed all occurrences of this syntax in Mathlib. + * As of [PR #13271](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12407), [PR #12547](https://github.com/leanprover-community/mathlib4/pull/12547), [PR #12947](https://github.com/leanprover-community/mathlib4/pull/12947), [PR #12408](https://github.com/leanprover-community/mathlib4/pull/12408), [PR #12597](https://github.com/leanprover-community/mathlib4/pull/12597), [PR #13185](https://github.com/leanprover-community/mathlib4/pull/13185), [PR #13182](https://github.com/leanprover-community/mathlib4/pull/13182), [PR #12598](https://github.com/leanprover-community/mathlib4/pull/12598), [PR #13188](https://github.com/leanprover-community/mathlib4/pull/13188), [PR #13368](https://github.com/leanprover-community/mathlib4/pull/13368). Note that within Mathlib you can use the newly introduced `deprecated alias` code snippet ([PR #13206](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/12515) whose output is available as a comment when tagging a PR with the new `move-decls` label (see [PR #12844](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/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](https://github.com/leanprover-community/mathlib4/pull/13164). + * 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](https://github.com/leanprover-community/mathlib4/pull/12777), [PR #12401](https://github.com/leanprover-community/mathlib4/pull/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` and `Int` 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 almost-circular import graph ricocheting between those three areas. The `Nat`- and `Int`-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 over-importing. The following PRs are steps towards that: [PR #11986](https://github.com/leanprover-community/mathlib4/pull/11986), [PR #12710](https://github.com/leanprover-community/mathlib4/pull/12710), [PR #12828](https://github.com/leanprover-community/mathlib4/pull/12828), [PR #12736](https://github.com/leanprover-community/mathlib4/pull/12736), [PR #12825](https://github.com/leanprover-community/mathlib4/pull/12825), [PR #12817](https://github.com/leanprover-community/mathlib4/pull/12817), [PR #12823](https://github.com/leanprover-community/mathlib4/pull/12823), [PR #12872](https://github.com/leanprover-community/mathlib4/pull/12872), [PR #12829](https://github.com/leanprover-community/mathlib4/pull/12829), [PR #12862](https://github.com/leanprover-community/mathlib4/pull/12862), [PR #12835](https://github.com/leanprover-community/mathlib4/pull/12835), [PR #12821](https://github.com/leanprover-community/mathlib4/pull/12821), [PR #12818](https://github.com/leanprover-community/mathlib4/pull/12818), [PR #12836](https://github.com/leanprover-community/mathlib4/pull/12836), [PR #12832](https://github.com/leanprover-community/mathlib4/pull/12832), [PR #12882](https://github.com/leanprover-community/mathlib4/pull/12882), [PR #12975](https://github.com/leanprover-community/mathlib4/pull/12975), [PR #11855](https://github.com/leanprover-community/mathlib4/pull/11855), [PR #13029](https://github.com/leanprover-community/mathlib4/pull/13029), [PR #12985](https://github.com/leanprover-community/mathlib4/pull/12985), [PR #13008](https://github.com/leanprover-community/mathlib4/pull/13008), [PR #13033](https://github.com/leanprover-community/mathlib4/pull/13033), [PR #12845](https://github.com/leanprover-community/mathlib4/pull/12845), [PR #12974](https://github.com/leanprover-community/mathlib4/pull/12974), [PR #11863](https://github.com/leanprover-community/mathlib4/pull/11863), [PR #12959](https://github.com/leanprover-community/mathlib4/pull/12959), [PR #13030](https://github.com/leanprover-community/mathlib4/pull/13030), [PR #13031](https://github.com/leanprover-community/mathlib4/pull/13031), [PR #13005](https://github.com/leanprover-community/mathlib4/pull/13005), [PR #13140](https://github.com/leanprover-community/mathlib4/pull/13140), [PR #13139](https://github.com/leanprover-community/mathlib4/pull/13139), [PR #12990](https://github.com/leanprover-community/mathlib4/pull/12990), [PR #13184](https://github.com/leanprover-community/mathlib4/pull/13184), [PR #13197](https://github.com/leanprover-community/mathlib4/pull/13197), [PR #13138](https://github.com/leanprover-community/mathlib4/pull/13138), [PR #12957](https://github.com/leanprover-community/mathlib4/pull/12957), [PR #13222](https://github.com/leanprover-community/mathlib4/pull/13222), [PR #13224](https://github.com/leanprover-community/mathlib4/pull/13224), [PR #13242](https://github.com/leanprover-community/mathlib4/pull/13242), [PR #13288](https://github.com/leanprover-community/mathlib4/pull/13288), [PR #13003](https://github.com/leanprover-community/mathlib4/pull/13003), [PR #13205](https://github.com/leanprover-community/mathlib4/pull/13205), [PR #13289](https://github.com/leanprover-community/mathlib4/pull/13289), [PR #13244](https://github.com/leanprover-community/mathlib4/pull/13244), [PR #13305](https://github.com/leanprover-community/mathlib4/pull/13305), [PR #13274](https://github.com/leanprover-community/mathlib4/pull/13274), [PR #13253](https://github.com/leanprover-community/mathlib4/pull/13253), [PR #13268](https://github.com/leanprover-community/mathlib4/pull/13268), [PR #13147](https://github.com/leanprover-community/mathlib4/pull/13147), [PR #13243](https://github.com/leanprover-community/mathlib4/pull/13243). \ No newline at end of file