March 2022 saw a record number of new contributions to mathlib: 682 PRs were merged, obliterating the old record of 565 merged PRs.

• Algebra.

  • After the definition of the Krull topology last month, PR #11973 and PR #12398 show the Krull topology is Hausdorff and totally disconnected
  • Joachim Breitner contributed to group theory by establishing the Ping Pong Lemma in PR #12210, then PR #11778 completes the last in a chain of equivalences for finite nilpotent groups (direct product of Sylow subgroups), culiminating in PR #11835.
  • PR #12866 A polynomial ring in arbitrarily many variables over a UFD is a UFD.
  • PR #12300 Adds non-unital and non-associative rings, thereby opening the door for applications elsewhere. For instance square matrices over a non-unital ring form a non-unital ring (PR #12913), non-unital normed rings (PR #12326), allow non-unital C∗-rings (PR #12327), and define unitization of a non-unital algebra (PR #12601).
  • PR #12041 Classifies 1d isocrystals in p-adic Hodge theory, and in so doing exhibits an application of the semilinear map refactor other than linear or conjugate-linear maps.
  • PR #12485 Adds a nice counterexample to mathlib: a homogeneous ideal that is not prime but homogeneously prime. This can only occur in graded rings that are graded by a non-cancellative monoid.
  • PR #12634 The three subgroups lemma

• Analysis

  • This month saw the initial development of bornology in mathlib, defined in PR #12036 by means of the cobounded filter instead of as a collection of bounded sets. This was followed closely by locally bounded maps (PR #12046), the category Born of bornologies (PR #12045) and the natural bornology of von Neumann bounded sets in a locally convex space (PR #12449 and PR #12721).
  • Convexity itself also had significant developments, including: closed balanced sets are a basis of the topology (PR #12786), the topology of weak duals is locally convex (PR #12623), and an inner product space is strictly convex (PR #12790).
  • Thanks to recent work in complex analysis, progress was made on the spectrum. Of particular interest are PR #12115 which shows that the spectrum in a complex Banach algebra is nonempty, and PR #12787 which proves the Gelfand-Mazur theorem.
  • PR #12329 Von Neumann algebras have landed in mathlib; Scott Morrison provided two definitions of a von Neumann algebra (concrete and abstract). There's still a long way to go before we can relate these definitions!
  • Integration theory saw PR #12216 which defines local integrability, PR #12539 shows continuous functions with exponential decay are integrable, and PR #12408 establishes uniform integrability and the Vitali convergence theorem.
  • In PR #12942 Sébastien Gouezel completed a vital refactor of the Bochner integral by removing the restriction of second countability on the codomain. This has the tremendous benefit of allowing the removal of assumptions of measurable_space, borel_space and second_countable_topology downstream.
  • Polish spaces were introduced in PR #12437 and then it was shown in PR #12448 that injective images of Borel sets in Polish spaces are Borel.
  • Sébastien Gouezel had another striking addition in PR #12492: change of variable formula in integrals in higher dimension. This particular formulation is notable for its generality.

• Category theory.

  • Jujian Zhang dualized the existing material on projective resolutions, and as a consequence we now have right derived functors and some basic properties (PR #12545, PR #12841 and PR #12810)
  • The coherence theorem (which we already had for monoidal categories) has been extended to bicategories, by Yuma Mizuno in PR #12155. We're now investigating writing tactics which make using coherence practical in proofs.

• Model theory. Continuing last month's inauguration of model theory in mathlib, this month saw

  • PR #12630 Notation for terms and formulas from Flypitch
  • PR #12531 Ultraproducts and the Compactness Theorem
  • PR #12837 Language equivalences

• Graph theory.

  • PR #10867 defines the incidence matrix of a simple graph.
  • Szemerédi's regularity lemma is slowly getting in. Building on edge density (PR #12431), PR #12958 defines the energy of a partition and PR #12957 introduces $\varepsilon$-regular partitions.

• Probability theory. Foundational work in probability theory occurred in:

  • PR #12678 Adds API for uniform integrability in the probability sense.
  • PR #12344 Defines conditional probability and adds basic related theorems.

• Number theory.

  • PR #12245 and PR #12715 add completion with respect to the place at infinity.
  • PR #12712 Adds the adic valuation on a Dedekind domain associated with a maximal ideal.
  • PR #12796 The Möbius function is multiplicative.

• Linear algebra.

  • PR #12767 The Weinstein–Aronszajn identity
  • PR #12438 The projectivization of a vector space.

• Algebraic geometry.

  • PR #12548 Irrelevant ideal of a graded algebra
  • PR #12635 Basic definitions of projective spectrum
  • PR #12784 Homogeneous localisation

• General. The community release of Lean was updated twice.

  • PR #12591 Updates to Lean 3.41.0c, which allows sorry to skip a tactic block, introduces the option pp.numeral_types to show numeral type ascriptions, and adds a search engine for finding relevant lemmas Lean PR #696.
  • PR #12818 Updates to Lean 3.42.0c, which includes a fix for the "unknown declaration" error when rebuilding oleans involving private definitions, and adds a noncomputable! modifier to completely inhibit VM compilation.