DerivedAlgGeo

DerivedAlgGeo is a Lean 4 library for derived algebraic geometry. Its current scope includes coherent sheaves and cohomology, dg and derived categories, Bridgeland stability conditions, duality, intersection theory, and Fourier--Mukai prerequisites.

The project is under active development. APIs may change as the formalization grows and relevant results are upstreamed to Mathlib.

Use

The complete stable library is available through one import:

import DerivedAlgGeo

Library code should prefer the narrowest useful subject import, such as:

import DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent
import DerivedAlgGeo.AlgebraicGeometry.DerivedCategory
import DerivedAlgGeo.AlgebraicGeometry.Moduli
import DerivedAlgGeo.CategoryTheory.Monoidal
import DerivedAlgGeo.Algebra.Homology.DGCategory
import DerivedAlgGeo.CategoryTheory.Triangulated.DGEnhancement
import DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Weak
import DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition

The repository is pinned to Lean and Mathlib v4.32.1. From a checkout, fetch the Mathlib cache and build the module you are working on:

lake exe cache get
LEAN_NUM_THREADS=2 lake build DerivedAlgGeo.The.Module.You.Changed

Full verification runs in CI, not on your machine. Opening a pull request runs the whole gate on ubuntu-latest; since 2026-09-19 a push on its own no longer does, and gh workflow run ci.yml --ref <branch> dispatches the self-hosted Windows lane when you want the platform check. A bare lake build and scripts/gates.sh are refused locally by a PreToolUse hook. For the local pre-flight the hook allows — every gate that needs no Lean build, plus a targeted build of what you changed, in seconds — run:

scripts/precheck.sh

See CONTRIBUTING.md §"Where verification runs". Note that scripts/gates.sh is neither a subset nor a superset of CI; that section has the verified table.

Layout

The source tree mirrors Mathlib's subject hierarchy, so a file extending a Mathlib API sits where that API sits in Mathlib. CLAUDE.md states the placement rule and docs/architecture/layers.md the dependency contract.

• DerivedAlgGeo/AlgebraicGeometry — schemes and everything stated about them: coherent sheaves, cohomology, scheme-derived categories and Dqc, geometric Fourier--Mukai kernels, stability on scheme-derived categories, semistable moduli, duality, intersection theory, Proj, and Riemann--Roch. Organized by geometric object; geometric realizations of categorical interfaces live here with the object they are about.
• DerivedAlgGeo/CategoryTheory — abelian, bicategorical, monoidal, and site theory; triangulated categories with t-structures, stability conditions, dg enhancements, Grothendieck groups, and Fourier--Mukai kernels.
• DerivedAlgGeo/Algebra — ring, module, and polynomial algebra; sheaves of modules on ringed sites under Algebra/Category/ModuleCat/Sheaf; derived categories, homotopy categories, dg categories, and spectral sequences under Algebra/Homology.
• DerivedAlgGeo/LinearAlgebra, RingTheory, Topology, AlgebraicTopology — reusable supporting mathematics at Mathlib's paths.
• DerivedAlgGeo/Analysis — the upper half-planes of ℂ, their argument geometry, and finite polygonal paths with the perimeter comparison under containment of vertex hulls. Neutral: nothing below it reaches a category, a scheme or a stability condition, and scripts/check_layering.py rule 13 keeps it that way.
• DerivedAlgGeo/Development — exploratory code outside the stable umbrella.

Generated API documentation is published at chris-dare-dev.github.io/derived-alg-geo-lean. See CONTRIBUTING.md for placement, proof, audit, and review requirements.

The enforced dependency contract is documented in docs/architecture/layers.md.

License

Repository-authored work is MIT-licensed. A small number of files derived from Mathlib or earlier Apache-2.0 work retain that license and attribution. See LICENSE.md for the complete scope and notices.