ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The algebra A_2 and its vertex projectives

Example

Take $m = 2$ , so that the doubled line quiver has vertices $0, 1, 2$ and arrows $(0 ∣ 1), (1 ∣ 2)$ and $(1 ∣ 0), (2 ∣ 1)$ , and let $A_{2}$ be the Khovanov–Seidel type A algebra of Khovanov–Seidel type A algebra. Then:

Basis. $A_{2}$ is free of rank $4 \cdot 2 + 1 = 9$ on the classes of the nine paths $(0), (1), (2), (0 ∣ 1), (1 ∣ 2), (1 ∣ 0), (2 ∣ 1), (1 ∣ 0 ∣ 1), (2 ∣ 1 ∣ 2),$ of internal degrees $0, 0, 0$ (vertices), $0, 0$ (ascending arrows), $1, 1$ (descending arrows) and $1, 1$ (returns). The relations specialised to $m = 2$ are $(0 ∣ 1 ∣ 2) = 0$ , $(2 ∣ 1 ∣ 0) = 0$ and $(0 ∣ 1 ∣ 0) = 0$ for the two compositions through the unique interior vertex $1$ and for the loop at $0$ , together with the single identification $(1 ∣ 2 ∣ 1) = (1 ∣ 0 ∣ 1)$ of the two returns at the interior vertex $1$ ; there is no relation involving a vertex $3$ .
Multiplication. Products of non-composable basis paths are $0$ , products of composable paths are their left-to-right concatenation, every concatenation of three or more arrows is $0$ in $A_{2}$ , and the two nontrivial length-two products are $(1 ∣ 0) (0 ∣ 1) = (1 ∣ 0 ∣ 1) = (1 ∣ 2 ∣ 1) = (1 ∣ 2) (2 ∣ 1), (2 ∣ 1) (1 ∣ 2) = (2 ∣ 1 ∣ 2),$ while $(0 ∣ 1) (1 ∣ 0) = (0 ∣ 1 ∣ 0) = 0$ and $(1 ∣ 2) (2 ∣ 1)$ has just been computed.
Vertex projectives. The left modules $P_{j} = A_{2} e_{j}$ are free $Z$ -modules on the paths ending at $j$ : $P_{0} = Z (0) \oplus Z (1 ∣ 0), P_{1} = Z (1) \oplus Z (0 ∣ 1) \oplus Z (2 ∣ 1) \oplus Z (1 ∣ 0 ∣ 1), P_{2} = Z (2) \oplus Z (1 ∣ 2) \oplus Z (2 ∣ 1 ∣ 2),$ of ranks $2, 4, 3$ and with graded ranks $P_{0} = (1, 1)$ , $P_{1} = (2, 2)$ , $P_{2} = (2, 1)$ in internal degrees $d = 0, 1$ . Ignoring all arrows gives $A_{2} / (arrows) = Z^{3}$ spanned by the three vertex idempotents.
Right projectives. Symmetrically $_{j} P = e_{j} A_{2}$ is free on the paths beginning at $j$ , so $_{0} P = Z (0) \oplus Z (0 ∣ 1)$ , $_{1} P = Z (1) \oplus Z (1 ∣ 0) \oplus Z (1 ∣ 2) \oplus Z (1 ∣ 0 ∣ 1)$ and $_{2} P = Z (2) \oplus Z (2 ∣ 1) \oplus Z (2 ∣ 1 ∣ 2)$ , again of ranks $2, 4, 3$ .

Facts & Assumptions

Given: The algebra $A_{2} = Z Γ_{2} / I_{2}$ with its nine-element path basis and its internal grading, the vertex idempotents $e_{0}, e_{1}, e_{2}$ , and the semigroup of composable paths of the doubled line quiver with vertices $0, 1, 2$ .

[F1]

$A_{m}$ for $m = 2$ is the quotient of the path ring $Z Γ_{2}$ by the two-sided ideal generated by $(i - 1 ∣ i ∣ i + 1)$ and $(i + 1 ∣ i ∣ i - 1)$ for $0 < i < 2$ , by $(i ∣ i + 1 ∣ i) - (i ∣ i - 1 ∣ i)$ for $0 < i < 2$ and by $(0 ∣ 1 ∣ 0)$ ; the internal degree is additive over concatenation with $\deg (i) = \deg (i ∣ i + 1) = 0$ and $\deg (i + 1 ∣ i) = 1$ (Khovanov–Seidel type A algebra).

[L2]

$A_{m}$ has the $Z$ -basis of $4 m + 1$ classes given by the vertices, the $2 m$ arrows and the returns $(1 ∣ 0 ∣ 1), \dots, (m ∣ m - 1 ∣ m)$ , so for $m = 2$ there are nine basis classes; every path of length at least three, every monotone length-two path in the interior and the return $(0 ∣ 1 ∣ 0)$ have class $0$ ; at the interior vertex $1$ the two returns agree (The 4m+1 path basis).

[L3]

The product of composable paths is their left-to-right concatenation and the product of non-composable paths is $0$ ; the unit is $\sum_{j} e_{j}$ , and $p$ lies in $P_{j} = A_{m} e_{j}$ exactly when $p$ ends at $j$ and in $_{j} P = e_{j} A_{m}$ exactly when $p$ begins at $j$ (Integral path ring of a finite quiver, Finite graded A_m-modules, internal shifts and the vertex projectives).

[L4]

The internal shift is degree raising, so a $Z$ -basis element of internal degree $d$ lies in the degree- $d$ component, and the graded rank of a free module counts basis elements per degree (Finite graded A_m-modules, internal shifts and the vertex projectives).

Proof

technique · direct

1.1

The nine basis paths and their degrees. Specialising [F1] to $m = 2$ lists the generators of $I_{2}$ as $(0 ∣ 1 ∣ 2)$ , $(2 ∣ 1 ∣ 0)$ , $(1 ∣ 2 ∣ 1) - (1 ∣ 0 ∣ 1)$ and $(0 ∣ 1 ∣ 0)$ , and by [L2] the classes of the vertices $(0), (1), (2)$ , the ascending arrows $(0 ∣ 1), (1 ∣ 2)$ , the descending arrows $(1 ∣ 0), (2 ∣ 1)$ and the returns $(1 ∣ 0 ∣ 1), (2 ∣ 1 ∣ 2)$ form a $Z$ -basis, nine classes in all; the degrees are $0$ for the vertices and ascending arrows and $1$ for the descending arrows by [F1], and $\deg (1 ∣ 0 ∣ 1) = \deg (1 ∣ 0) + \deg (0 ∣ 1) = 1 + 0 = 1$ , $\deg (2 ∣ 1 ∣ 2) = 1 + 0 = 1$ by the additivity of the degree over concatenation.

F1L2

1.2

The vanishing and identification rules at $m = 2$ . By [F1] the monotone length-two paths $(0 ∣ 1 ∣ 2)$ and $(2 ∣ 1 ∣ 0)$ have class $0$ , while by [L2] every path of length at least three has class $0$ ; the return $(0 ∣ 1 ∣ 0)$ has class $0$ ; and the two returns at the interior vertex $1$ satisfy $(1 ∣ 2 ∣ 1) = (1 ∣ 0 ∣ 1)$ with no further relation, because the only interior vertex is $1$ .

F1L2

2.1

The multiplication table. Products of non-composable paths vanish and products of composable paths are concatenations by [L3]. For length two: $(1 ∣ 0) (0 ∣ 1) = (1 ∣ 0 ∣ 1)$ and $(1 ∣ 2) (2 ∣ 1) = (1 ∣ 2 ∣ 1) = (1 ∣ 0 ∣ 1)$ by step 1.2, $(2 ∣ 1) (1 ∣ 2) = (2 ∣ 1 ∣ 2)$ , and $(0 ∣ 1) (1 ∣ 0) = (0 ∣ 1 ∣ 0) = 0$ by step 1.2; every product of two classes that are not composable, and every product of three or more nonvanishing arrows, is either a non-composable product or a path of length at least three and hence $0$ . In particular $A_{2}$ is not commutative, since $(1 ∣ 0) (0 ∣ 1) = (1 ∣ 0 ∣ 1) \neq 0$ while $(0 ∣ 1) (1 ∣ 0) = 0$ .

step 1.1step 1.2L3

2.2

The quotient by the arrows is $Z^{3}$ . The two-sided ideal generated by the arrows consists of the $Z$ -linear combinations of the basis elements that are not vertices, and the vertex idempotents multiply by $e_{j} e_{k} = δ_{j k} e_{j}$ by [L3]; hence the quotient $A_{2} / (arrows)$ is free of rank $3$ on the classes of $e_{0}, e_{1}, e_{2}$ and is isomorphic to $Z^{3}$ as a ring with coordinatewise multiplication.

step 1.1L3

2.3

The vertex projectives. By [L3] the module $P_{j} = A_{2} e_{j}$ is spanned over $Z$ by the nine basis paths that end at $j$ , and by step 1.1 those are, for $j = 0$ : $(0)$ and $(1 ∣ 0)$ ; for $j = 1$ : $(1)$ , $(0 ∣ 1)$ , $(2 ∣ 1)$ and $(1 ∣ 0 ∣ 1)$ ; for $j = 2$ : $(2)$ , $(1 ∣ 2)$ and $(2 ∣ 1 ∣ 2)$ . Since the nine classes are $Z$ -linearly independent by step 1.1, each of these lists is a $Z$ -basis, so the ranks are $2, 4, 3$ as displayed, and their degrees read off from step 1.1 give the graded ranks $(1, 1)$ , $(2, 2)$ and $(2, 1)$ in internal degrees $0$ and $1$ by [L4].

step 1.1L3L4

2.4

The right modules $_{j} P$ . Symmetrically, $_{j} P = e_{j} A_{2}$ is spanned by the basis paths beginning at $j$ , namely $(0), (0 ∣ 1)$ for $j = 0$ ; $(1), (1 ∣ 0), (1 ∣ 2), (1 ∣ 0 ∣ 1)$ for $j = 1$ ; and $(2), (2 ∣ 1), (2 ∣ 1 ∣ 2)$ for $j = 2$ , the same lists with the roles of the arrow directions exchanged; these are bases by step 1.1, so the ranks are again $2, 4, 3$ .

step 1.1L3

3.1

Conclusion. At $m = 2$ the algebra $A_{2}$ has the nine-element path basis of step 1.1 with the multiplication of step 2.1 and the vanishing rules of step 1.2; the vertex projectives $P_{0}, P_{1}, P_{2}$ are free of ranks $2, 4, 3$ on the paths ending at $0, 1, 2$ with graded ranks $(1, 1), (2, 2), (2, 1)$ , and the right modules $_{j} P$ are free of the same ranks on the paths beginning at $j$ ; the quotient by the arrow ideal is $Z^{3}$ by step 2.2. All computations are finite lists of the nine basis paths, and no choice principle is used.

step 2.1step 2.2step 2.3step 2.4∎

Depends on

Used by

An explicit projective resolution of the vertex module S₂ for A₂ Example

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Mikhail Khovanov and Paul Seidel, Quivers, Floer Cohomology, and Braid Group Actions, §1b, printed pp. 3-4 (standard reference, not scraped)