A∞ Categories in Lean
Marco David, Jason Dong, Hallvard Hareide, Jasper van de Kreeke, Lillian Liu, Justin Mu, Zhan Shi, Niels Voss, Annie Yao
Repository for the formalization of
Check out the blueprint homepage for this project.
Repository structure
The Lean sources are split into four Lake libraries. Each has a root file
(Util.lean, ComputableCochainComplex.lean, AInfinity.lean, KLRW.lean) that imports every
file in the corresponding folder; these root files are generated by lake exe mk_all
and checked in CI, so rerun that command after adding a file.
| Folder | Contents |
|---|---|
Util/ | Contains a Texify class and the #texify command for rendering terms as LaTeX. |
ComputableCochainComplex/ | Computable categorical constructions: explicit biproducts and zero objects, the computable additive completion CMat_, and bounded cochain complexes. |
AInfinity/ | Gradings and their homomorphisms, graded linear maps, graded linear quivers, the Stasheff identities, A∞-categories, A∞-categories with vanishing higher operations, DG and linear categories as A∞-categories, A∞-functors. |
KLRW/ | KLRW algebras and categories: the general quiver-parametrised KLRW algebra and its |
The blueprint sources live in blueprint/src/. The API documentation is built on CI by
docgen-action, which generates a docbuild/ project depending on doc-gen4 at the tag of
the current Lean toolchain; the checked-in docbuild/lakefile.toml is its local counterpart.
Project metadata and license
formalization.yaml records the project's sources, scope, status,
fidelity to the literature, and how it was produced, following the
community standards.
Please keep it up to date (e.g. the sorry counts and scope) when making significant
changes; CI validates it against the schema.
The code is released under the Apache 2.0 license; see LICENSE.