Skip to main content

This month in mathlib (Aug 2021)

Source

This post summarizes some of the activity that happened in mathlib in August.

Highlighted PRs

  • PR #8652: chore(*): update lean to 3.32.1
    The community fork of Lean made two new releases 3.32.0 and 3.32.1. This is part of the preparations for porting mathlib to Lean 4.

  • PR #8281: continuous and smooth partition of unity
    See the companion blogpost for details.

  • Radon-Nikodym and Lebesgue decomposition. The four PRs PR #8645 PR #8687 PR #8763 PR #8875 together contribute the Lebesgue decomposition for sigma-finite measures and the Radon-Nikodym theorem.

  • PR #7978: strong version of FTC-2
    This weakens considerably the assumptions of part of the fundamental theorem of calculus: $\int _{a}^{b}f'(x)\,dx=f(b)-f(a)$, replacing continuity of $f'$ by the much more natural assumption of integrability.

  • PR #4885: general adjoint functor theorem: If $G : D ⇒ C$ preserves limits and $D$ has limits, and satisfies the solution set condition, then it has a left adjoint.

  • PR #8692: finite fields exist
    Most of this PR had been lying around for ages, but it was finally put together in mathlib. It shows the existence and uniqueness up to isomorphism of a finite field with cardinal $p^n$ for any prime number $p$ and positive integer $n$.

  • Among several PRs from the Dedekind project, the two most noteworthy are

    • PR #8530: ideals in a Dedekind domain have unique factorization
    • PR #8626: define the ideal class group

  • PR #8377: new file
    This PR defines the complex upper half plane, together with the $\mathrm{SL}_2$-action.
    Upcoming PRs will characterize the fundamental domain of the $\mathrm{SL}_2(\mathbb{Z})$-action.

Other mathematical contributions

The following PRs are ordered by the date that they were merged into mathlib.

  • PR #8424: prove that complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential
  • PR #8560: Add the Kronecker product
  • PR #8388: signed version of the Hahn decomposition theorem
  • PR #8588: Smith normal form for submodules over a PID This PR is a step towards the classification of finite type modules over a PID.
  • PR #8266: Stieltjes measures associated to monotone functions
  • PR #8598: add definition and first lemmas about weak-star topology
  • PR #8639: prove Haar measure = Lebesgue measure on $ℝ$
  • PR #8558: add working definition of elliptic curve
  • PR #8538: add nilpotent groups
  • PR #8343: generalize inequalities and invariance of dimension to arbitrary rings
  • PR #8791: volume of a (closed) $L^∞$-ball
  • PR #8576: define exponential in a Banach algebra and prove basic results