Skip to main content

This month in mathlib (Nov 2021)

Source

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

  • Geometry and algebraic topology.

    • The series PR #10284, PR #10297, PR #10303, PR #10328, PR #10334, and PR #10401 constructs the sheafification of presheaves with respect to a Grothendieck topology on a category, culminating with a construction of colimits in the category SheafedSpace. It is an important building block in setting up algebraic geometry, as well as a requirement for the Liquid Tensor Experiment (LTE). A corollary is that the category of sheaves with values in a suitable concrete abelian category is itself an abelian category. This has been formalised for LTE, and should appear in mathlib in the near future.
    • Barycentric coordinates have been further studied in a series of PRs including for instance PR #10320 relating them to determinants.
    • PR #10381 proves the orthogonal group is generated by reflections.
    • PR #10195 defines the fundamental groupoid, as functor from Top to Groupoid.

  • Number theory.

    • PR #9071 defines the class number of number fields and function fields. This finishes the finiteness proof of the class group of a number field and function field, described in a previous blog post.
    • PR #8820 adds Lucas primality test.

  • Group theory.

    • PR #10059 proves that (infinite) Sylow subgroups are isomorphic.
    • PR #10283 proves the full Schur-Zassenhaus theorem.
    • PR #10249 defines the exponent of a group.

  • Combinatorics.

  • Linear algebra and functional analysis

    • The sequence of PRs PR #9840, PR #9995, PR #10317 establishes the connection between eigenvalues and the Rayleigh quotient, and proves the diagonalization theorem for self-adjoint endomorphisms on finite-dimensional inner product spaces.
    • PR #10145 introduces $C^*$-algebras.
    • PR #10530 proves properties of spectrum in a Banach algebra.
    • PR #9097 defines the Minkowski gauge functional.

  • Analysis

    • PR #9791 proves the Picard-Lindelöf/Cauchy-Lipschitz theorem about ordinary differential equations.
    • PR #10057 defines Vitali families and PR #10101 shows the main theorem on differentiation of measures: given two measures ρ and μ on a finite-dimensional real vector space, the ratio ρ (ball x r) / μ (ball x r) converges μ-almost everywhere to the Radon-Nikodym derivative of ρ with respect to μ when r tends to 0. The theorem is in fact proved in the more general context of Vitali families, as in Federer's famous book on geometric measure theory.
    • PR #10073 proves convergence of a sequence which does not oscillate infinitely.
    • PR #10258 proves that, if $u_n$ is subadditive, then $u_n / n$ converges.