A_∞ Categories in Lean

by Marco David, Jason Dong, Hallvard Hareide, Jasper van de Kreeke, Justin Mu, Niels Voss, and Annie Yao

Online Blueprint Blueprint as PDF Documentation GitHub

Overview

This project provides a Lean formalization of \(A_\infty\)-categories, functors between them and natural transformations. Moreover, we implement the braid group action on modules over quiver Hecke algebras (KLRW algebras) algorithmically, which provides an exciting & computable example of an \(A_\infty\)-functor at the intersection of symplectic geometry, representation theory and homological algebra. This is work in progress.

We collaborate using the Lean Zulip chat. There is also an evolving dependency graph of our definitions and theorems.

Maintainers

See the GitHub repository for full contributor list and issue tracker.