Persistence Module Diagram Chaser

Double-click the grid to add a module · Shift-drag (or Arrow mode) between modules to add a map

How it works

Modules: double-click an empty grid cell. Drag to move. Kinds: general, free, 0. All modules are finitely generated k[t]-modules.
Maps: Shift-drag from one module to another (or switch to Arrow mode). Set injective ↪, surjective ↠, isomorphism ≅ (both), zero, identity = (double line: the two modules are the same module and the map is its identity — stronger than ≅, which is just some invertible map), or induced ∃! (dashed: a map to be constructed from the rest of the diagram, by factoring through an injective/surjective map or along a zigzag of maps and preimages, like the snake lemma's connecting map).
ker / im / coker: select a map and add its kernel, image or cokernel. They come with their universal maps (ι, e/m, π) and exactness.
Exactness & squares: Shift-click several maps. A composable chain can be marked exact (every inner spot) or turned into a new map equal to its composite ("Add composite", e.g. g∘f); four maps forming a square can be marked pullback or pushout.
Commutativity: every diagram is assumed to commute (all parallel composites of solid maps agree).
Queries run an element-wise diagram chase. A proof is shown in words and as a Lean 4 / Mathlib theorem. If the chase saturates without a proof, the saturated state is a finite-dimensional counterexample (over ℚ, with t acting as 0).

Run it locally

Everything runs in your browser; only checking proofs with your own Lean needs the small bundled server. Python 3 is enough to run the app; Lean is optional.

Get the code: git clone https://github.com/primozskraba/diagram-chaser (or download it as a ZIP from GitHub), then cd diagram-chaser.
Start it: python3 server.py and open http://127.0.0.1:8765.
For proof checking, install Lean with elan and, inside diagram-chaser, make a Mathlib project once: lake +leanprover-community/mathlib4:lean-toolchain new lean-project math, then cd lean-project && lake exe cache get && cd ... (An existing Mathlib project works too: python3 server.py --lean-project PATH.)
Restart python3 server.py: it finds lean-project, and “Check with local Lean” and “verify with Lean” are enabled.
To check a downloaded proof by hand: cd lean-project && lake env lean ~/Downloads/DiagramChase.lean (no errors means Lean accepted it).

If the browser saves the download with another name or extension (e.g. DiagramChase.lean.txt), rename it or pass that name to lake env lean; the file is plain text, and “Copy Lean” works too.

Hypotheses

Query

verify with Lean