Lie theory

Co-authored-by: Oliver Nash <[email protected]>

posts/month-in-mathlib-may-2024.md

@@ -18,24 +18,13 @@ There were 667 PRs merged in May 2024.
 <!-- TEASER_END -->
 
 * Algebra
-  * In Lie theory, [PR #12297](https://github.com/leanprover-community/mathlib4/pull/12297) proves that any finite-dimensional Lie algebra over an infinite field contains a Cartan subalgebra (in fact many). [PR #12937](https://github.com/leanprover-community/mathlib4/pull/12937) proves that the root spaces of a semisimple Lie algebra relative to a splitting Cartan subalgebra are 1-dimensional, and [PR #13307](https://github.com/leanprover-community/mathlib4/pull/13307) proves that the roots of a semisimple Lie algebra are actually an abstract (reduced, crystallographic) root system.
+  * 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.
   * Joël Riou
     * [PR #12713](https://github.com/leanprover-community/mathlib4/pull/12713) :: feat(Algebra/Category/ModuleCat): the category of presheaves of modules has colimits
 * 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.
-  * Oliver Nash
-    * [PR #13208](https://github.com/leanprover-community/mathlib4/pull/13208) :: feat: equality of coroots implies equality of roots for Lie algebras
-    * [PR #13298](https://github.com/leanprover-community/mathlib4/pull/13298) :: feat(Algebra/Lie/Weights): `n` such that `n • α + β` is a weight is consecutive.
-    * [PR #13217](https://github.com/leanprover-community/mathlib4/pull/13217) :: feat(Algebra/Lie/Semisimple): API for semisimple Lie algebras
-    * [PR #13370](https://github.com/leanprover-community/mathlib4/pull/13370) :: chore(Algebra/Lie/Abelian): a nonabelian atomic Lie ideal is perfect
-    * [PR #13387](https://github.com/leanprover-community/mathlib4/pull/13387) :: chore(Algebra/Lie/Submodule): the lattice of Lie submodules is atomic
-    * [PR #13391](https://github.com/leanprover-community/mathlib4/pull/13391) :: feat(Algebra/Lie/InvariantForm): Lie algebras with a nondegenerate invariant form are semisimple
-    * [PR #13265](https://github.com/leanprover-community/mathlib4/pull/13265) :: feat(Algebra/Lie): Killing Lie algebras are semisimple
-    * [PR #13179](https://github.com/leanprover-community/mathlib4/pull/13179) :: feat: add lemma `LieAlgebra.IsKilling.span_weight_isNonZero_eq_top`
-    * [PR #12712](https://github.com/leanprover-community/mathlib4/pull/12712) :: feat: Cartan subalgebras contain only semisimple elements if the Killing form is non-singular and the coefficients are a perfect field.
-    * [PR #13076](https://github.com/leanprover-community/mathlib4/pull/13076) :: feat: define `sl₂` triples and prove basic result
   * Jz Pan
     * [PR #13322](https://github.com/leanprover-community/mathlib4/pull/13322) :: feat: add the definition of `OrzechProperty`
   * Scott Carnahan