diff --git a/posts/month-in-mathlib-oct-nov-2022.md b/posts/month-in-mathlib-oct-nov-2022.md new file mode 100644 index 0000000..7226faf --- /dev/null +++ b/posts/month-in-mathlib-oct-nov-2022.md @@ -0,0 +1,87 @@ +--- +author: '' +category: '' +date: 2022-12-01 14:56:21 UTC+01:00 +description: '' +has_math: true +link: '' +slug: this-month-in-mathlib-oct-and-nov-2022 +tags: '' +title: This month in mathlib (Oct and Nov 2022) +type: text +--- +In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below. + +* Measure theory. + - [PR #16830](https://github.com/leanprover-community/mathlib/pull/16830) improves Vitali families and Lebesgue density theorem. + - [PR #16762](https://github.com/leanprover-community/mathlib/pull/16762) adds a version of Lebesgue's density theorem. + - [PR #16906](https://github.com/leanprover-community/mathlib/pull/16906) proves Lebesgue differentiation theorem. + - [PR #16836](https://github.com/leanprover-community/mathlib/pull/16836) relates integrals over `add_circle` with integrals upstairs in `ℝ`. + +* Algebra. + - [PR #14672](https://github.com/leanprover-community/mathlib/pull/14672) defines mixed/equal characteristic zero. + - [PR #17018](https://github.com/leanprover-community/mathlib/pull/17018), [PR #16849](https://github.com/leanprover-community/mathlib/pull/16849) and [PR #17011](https://github.com/leanprover-community/mathlib/pull/17011) show the Kähler differential module is functorial and that $S/R$ is formally unramified if and only if $\Omega^1_{S/R} = 0$. They also give the standard presentation of the Kähler differential module. + - [PR #16000](https://github.com/leanprover-community/mathlib/pull/16000) proves Artin-Rees lemma and Krull's intersection theorems. + - [PR #16317](https://github.com/leanprover-community/mathlib/pull/16317) adds the multinomial theorem. + - [PR #17295](https://github.com/leanprover-community/mathlib/pull/17295) proves the Jordan-Hölder theorem for modules. + - [PR #17311](https://github.com/leanprover-community/mathlib/pull/17311) proves that a group with finitely many commutators has finite commutator subgroup. + - [PR #17243](https://github.com/leanprover-community/mathlib/pull/17243) proves the Third Isomorphism theorem for rings. + - [PR #13749](https://github.com/leanprover-community/mathlib/pull/13749) introduces non-unital subsemirings. + +* Analysis + - [PR #16723](https://github.com/leanprover-community/mathlib/pull/16723) shows that two analytic functions that coincide locally coincide globally. + - [PR #16683](https://github.com/leanprover-community/mathlib/pull/16683) and [PR #16680](https://github.com/leanprover-community/mathlib/pull/16680) introduce functions of bounded variation and prove that they are almost everywhere differentiable. As a corollary, [PR #16549](https://github.com/leanprover-community/mathlib/pull/16549) shows that a monotone function is differentiable almost everywhere. + - [PR #17119](https://github.com/leanprover-community/mathlib/pull/17119) defines and gives basic properties of the complex unit disc. + - [PR #16780](https://github.com/leanprover-community/mathlib/pull/16780) proves the open mapping theorem for holomorphic functions. + - [PR #16487](https://github.com/leanprover-community/mathlib/pull/16487) constructs the volume form. + - [PR #16796](https://github.com/leanprover-community/mathlib/pull/16796) generalizes the Hahn-Banach separation theorem to (locally convex) topological vector spaces. + - [PR #16835](https://github.com/leanprover-community/mathlib/pull/16835) proves functoriality of the character space. + - [PR #16638](https://github.com/leanprover-community/mathlib/pull/16638) introduces the Dirac delta distribution. + - [PR #17110](https://github.com/leanprover-community/mathlib/pull/17110) proves smoothness of series of functions. + - [PR #16201](https://github.com/leanprover-community/mathlib/pull/16201) and [PR #17598](https://github.com/leanprover-community/mathlib/pull/17598) define the additive circle and develop Fourier analysis on it. + - [PR #17543](https://github.com/leanprover-community/mathlib/pull/17543) computes $\Gamma(1/2)$. + - [PR #16053](https://github.com/leanprover-community/mathlib/pull/16053) topology/algebra/module/strong_operator, analysis/normed_space/operator_norm: strong operator topology. + +* Number theory. + - [PR #15405](https://github.com/leanprover-community/mathlib/pull/15405) introduces the Selmer group of a Dedekind domain. + - [PR #17677](https://github.com/leanprover-community/mathlib/pull/17677) defines slash-invariant forms, a step towards the definition of modular forms. + - [PR #17203](https://github.com/leanprover-community/mathlib/pull/17203) defines the absolute ideal norm. + +* Representation theory. + - [PR #17005](https://github.com/leanprover-community/mathlib/pull/17005) is about exactness properties of resolutions. + - [PR #16043](https://github.com/leanprover-community/mathlib/pull/16043) proves the orthogonality of characters. + - [PR #13794](https://github.com/leanprover-community/mathlib/pull/13794) proves Schur's lemma. + - [PR #17443](https://github.com/leanprover-community/mathlib/pull/17443) adds the construction of a projective resolution of a representation. + +* Topology. + - [PR #16677](https://github.com/leanprover-community/mathlib/pull/16677) constructs the Galois correspondence between closed ideals in $C(X, 𝕜)$ and open sets in $X$. + - [PR #16719](https://github.com/leanprover-community/mathlib/pull/16719) shows that maximal ideals of $C(X, 𝕜)$ correspond to (complements of) singletons. + - [PR #16087](https://github.com/leanprover-community/mathlib/pull/16087) defines covering spaces. + - [PR #16797](https://github.com/leanprover-community/mathlib/pull/16797) proves that the stalk functor preserves monomorphism. + - [PR #17015](https://github.com/leanprover-community/mathlib/pull/17015) proves that Noetherian spaces have finite irreducible components. + +* Probability theory. + - [PR #16882](https://github.com/leanprover-community/mathlib/pull/16882) proves the second Borel-Cantelli lemma. + - [PR #16648](https://github.com/leanprover-community/mathlib/pull/16648) shows Kolmogorov's 0-1 law. + +* Algebraic and differential geometry. + - [PR #16124](https://github.com/leanprover-community/mathlib/pull/16124), [PR #17117](https://github.com/leanprover-community/mathlib/pull/17117), [PR #17080](https://github.com/leanprover-community/mathlib/pull/17080) and [PR #17184](https://github.com/leanprover-community/mathlib/pull/17184) develop various properties for morphisms of schemes. + +* Linear algebra. + - [PR #11468](https://github.com/leanprover-community/mathlib/pull/11468) shows that the clifford algebra is isomorphic as a module to the exterior algebra. + - [PR #16150](https://github.com/leanprover-community/mathlib/pull/16150) proves that the inverse of a block triangular matrix is block triangular. + +* Category theory. + - [PR #16969](https://github.com/leanprover-community/mathlib/pull/16969) adds basic results about localization of categories. + +* Combinatorics + - [PR #16195](https://github.com/leanprover-community/mathlib/pull/16195) adds the definition and some basic results about semistandard Young tableaux. + - [PR #17445](https://github.com/leanprover-community/mathlib/pull/17445) combinatorics/young: add equivalence between Young diagrams and lists of natural numbers. + +* Tactics + - [PR #16313](https://github.com/leanprover-community/mathlib/pull/16313) introduces the `qify` tactic, to move from $\mathbb{Z}$ to $\mathbb{Q}$. + - [PR #13483](https://github.com/leanprover-community/mathlib/pull/13483) adds a tactic for moving around summands. + - [PR #16911](https://github.com/leanprover-community/mathlib/pull/16911) adds a tactic to find declarations that use `sorry`. This tactic is intended for projects that depend on mathlib. + + +During this months, we got two new versions of Lean. We also started to systematically port mathlib to Lean4, see the [wiki](https://github.com/leanprover-community/mathlib4/wiki). \ No newline at end of file