• Liquid Tensor Experiment is the work-in-progress on Peter Scholze's challenge to formalise an important milestone theorem from his work with Dustin Clausen. See his guest blog post on the Xena Project blog.

    It's also a nice pun on a progressive metal band's name.

  • Grothendieck's schemes in algebraic geometry is another update from the formalisation crowd, but now not from the Lean users (not this one), and rather from Isabelle users. They've successfully implemented schemes and proven some foundational results about them. Exciting times!

  • Dylan Spence: A note on semiorthogonal indecomposability of some Cohen–Macaulay varieties discusses the indecomposability of two flavours of the derived category (perfect complexes resp. bounded derived category of coherent sheaves) of singular varieties. For a Cohen–Macaulay variety the dualizing complex is a sheaf, and one can talk about its base locus. Dylan shows that the Kawatani–Okawa result for indecomposability of derived categories of smooth varieties with finite canonical base locus generalises to this setting, suitably replacing skyscrapers of possibly singular points by Koszul zero-cycles, which define perfect complexes with support a closed point. Cool stuff!