This is a Lean formalization of Chapters 1–7 of Fomin, Williams and Zelevinsky's Introduction to Cluster Algebras.
- Mutating a quiver and then taking its extended exchange matrix agrees with mutating the matrix.
- Matrix mutation preserves the determinant when the mutated diagonal entry vanishes.
- Matrix mutation preserves the rank when the mutated diagonal entry vanishes.
- Matrix mutation preserves the gcd of the entries, assuming mutation in that direction is an involution.
- A skew-symmetrizing vector of a matrix with connected diagram is unique up to a scalar.
- The Markov quiver is isomorphic to each of its mutations.
- The arrows between the chambers of a wiring diagram form a quiver.
- A braid move of a wiring diagram mutates its quiver.
- A double wiring diagram on
n + 2strands has(n + 2)²chambers,(n + 1)²of them bounded. - Orientations of non-isomorphic finite trees are not mutation equivalent, assuming the Caldero–Keller theorem.
- A seed pattern is of finite type if and only if one of its exchange matrices has a Cartan counterpart of finite type, assuming the Cartan–Killing classification and exercises of FWZ.
See §Formal Challenge for a formal certificate.
This depends on Mathlib.
A formal challenge file certifying that this repository does formalize the results claimed above is located at Challenge/Basic.lean. This file only depends on Mathlib. It contains formal statements of §Main Results with sorry as proof.
This repository can be verified against the formal challenge with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator. Then, run the following command:
lake comparator --config Comparator/comparator.json
This repository has been locally verified with the comparator, using Lean's kernel and nanoda. An earlier run with --paranoid also accepted it with Lean's paranoid checker, lean4lean and con-leche; con-ron could not complete within the machine's memory on this export.