3 papers
math.AG2026
High Frobenius pushforwards generate the bounded derived category
Matthew R. Ballard, Srikanth B. Iyengar, Pat Lank +2
This work concerns generators for the bounded derived category of coherent sheaves over a noetherian scheme of prime characteristic. The main result is that when the Frobenius…
math.AG2025
King's Conjecture and the Cox category
Matthew R. Ballard, Christine Berkesch, Michael K. Brown +6
We state and prove a realization of King's Conjecture for a category glued from the derived categories of all of the toric varieties arising from a given Cox ring. Our perspective…
cs.PL2025
Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin +3
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for ch…