TheoremStatement: Literature-sourcedProof: 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.

Corner computations: the U_i satisfy the Temperley-Lieb relations

Statement

Fix $m \geq 1$ , and for $1 \leq i \leq m$ let $U_{i} = P_{i} \otimes_{Z}_{i} P$ be the graded $(A_{m}, A_{m})$ -bimodule of The two-sided projective bimodules U_i and their tensor functors, with the tensor functor $U_{i} (-) = U_{i} \otimes_{A_{m}} -$ on the category $A_{m} -mod$ of Finite graded A_m-modules, internal shifts and the vertex projectives.

Square. For every $1 \leq i \leq m$ there is an isomorphism of graded $(A_{m}, A_{m})$ -bimodules $U_{i} \otimes_{A_{m}} U_{i} ≅ U_{i} \oplus U_{i} {1},$ hence an isomorphism of graded functors $U_{i} U_{i} ≅ U_{i} \oplus U_{i} {1}$ natural in the argument module.
Triple. For every $1 \leq i \leq m$ with $1 \leq i \pm 1 \leq m$ there is an isomorphism of graded $(A_{m}, A_{m})$ -bimodules $U_{i} \otimes_{A_{m}} U_{i \pm 1} \otimes_{A_{m}} U_{i} ≅ U_{i} {1},$ again natural as an isomorphism of graded functors.
Orthogonality. If $∣ i - j ∣ > 1$ then $U_{i} \otimes_{A_{m}} U_{j} = 0$ as a graded bimodule, so $U_{i} U_{j}$ is the zero functor.

Here $U_{i} U_{j}$ abbreviates the composite tensor functor $M \mapsto U_{i} \otimes_{A_{m}} (U_{j} \otimes_{A_{m}} M)$ , which is identified with $(U_{i} \otimes_{A_{m}} U_{j}) \otimes_{A_{m}} -$ by the associativity isomorphism of Graded associativity, units, and internal-shift tensor isomorphisms. The three families are the Temperley–Lieb relations of the source in the form needed on this page; they do not assert the braid relations between the invertible complexes $R_{i}$ , which belong to a later stage.

Facts & Assumptions

Given: An integer $m \geq 1$ , the algebra $A_{m}$ with vertices $(j)$ , arrows $(j ∣ j \pm 1)$ and returns $(j ∣ j - 1 ∣ j)$ , the vertex projectives $P_{i} = A_{m} e_{i}$ and $_{i} P = e_{i} A_{m}$ , and indices $1 \leq i, j \leq m$ .

[F1]

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

[L2]

The classes of the $m + 1$ vertices, the $2 m$ arrows $(j ∣ j \pm 1)$ and the $m$ returns $(j ∣ j - 1 ∣ j)$ for $1 \leq j \leq m$ form a $Z$ -basis of $A_{m}$ ; every path of length at least three has class $0$ , the monotone and reverse monotone length-two paths have class $0$ , the return $(0 ∣ 1 ∣ 0)$ has class $0$ , and at an interior vertex the two returns have the same class (The 4m+1 path basis).

[L3]

$A_{m}$ is graded by internal degree with $\deg e_{j} = \deg (j ∣ j + 1) = 0$ and $\deg (j + 1 ∣ j) = 1$ , additively over concatenation, and $A_{m} -mod$ is abelian with degreewise kernels and cokernels; the internal shift $M {r}$ is an automorphism and every $P_{j}$ and $_{j} P$ is finite graded projective, generated by $e_{j}$ (Khovanov–Seidel type A algebra, Finite graded A_m-modules, internal shifts and the vertex projectives).

[L4]

For graded bimodules over graded algebras the balanced tensor is associative, the tensor-unit maps $R \otimes_{R} N \to N$ and $M \otimes_{R} R \to M$ are degree-zero isomorphisms compatible with outer actions, and $M {r} \otimes_{R} N {s} ≅ (M \otimes_{R} N) {r + s}$ naturally (Graded associativity, units, and internal-shift tensor isomorphisms).

[L5]

The balanced tensor of graded modules carries the total-degree grading in which a homogeneous elementary tensor has degree the sum of the degrees of its factors, and outer actions make it a graded module on the appropriate side (Graded balanced tensor product and homogeneous Hom).

[L6]

If a graded $(B, A)$ -bimodule $M$ is flat as an underlying right $A$ -module, then $M \otimes_{A} -$ is exact on graded left $A$ -modules (Bimodule tensor exactness and preservation of finite projectives have separate hypotheses).

[F7]

Every projective left or right module over an arbitrary unital ring is flat on its side, without the Axiom of Choice (Projective left and right modules are flat over an arbitrary ring).

[L8]

A graded module is finite graded projective if and only if it is a degree-zero direct summand of a finite direct sum of internal shifts of the regular module, and every direct summand of a projective object is projective (Finite graded projectives are finite shifted-free summands, A direct summand of a projective is projective).

Proof

technique · direct

1.1

Corners. For $0 \leq i, j \leq m$ the graded abelian group $e_{i} A_{m} e_{j}$ has $Z$ -basis consisting of the classes of the paths from $i$ to $j$ of length at most two: the vertex $e_{i}$ when $j = i$ , the arrow $(i ∣ i + 1)$ when $j = i + 1$ , the arrow $(i ∣ i - 1)$ when $j = i - 1$ , and the return $(i ∣ i - 1 ∣ i)$ when $j = i \geq 1$ ; in particular $e_{i} A_{m} e_{j} = 0$ whenever $∣ i - j ∣ > 1$ , and $e_{i} A_{m} e_{i} = Z e_{i} \oplus Z (i ∣ i - 1 ∣ i)$ is free of rank $2$ for $1 \leq i \leq m$ , while $e_{0} A_{m} e_{0} = Z e_{0}$ has rank $1$ . Indeed every basis path of [L2] of length $\leq 2$ has prescribed source and target, the length-two basis elements are the returns $(1 ∣ 0 ∣ 1), \dots, (m ∣ m - 1 ∣ m)$ , all other length-two paths are $0$ in $A_{m}$ by [L2], and all longer paths vanish by [L2].

L2F1

2.1

The tensor cancellation $_{i} P \otimes_{A_{m}} P_{j} ≅ e_{i} A_{m} e_{j}$ . By [L3] the module $_{i} P$ is finite graded projective on the right, hence its underlying ungraded right $A_{m}$ -module is a degree-zero direct summand of a finite direct sum of shifts of $A_{m}$ by [L8], hence is a direct summand of a free module and projective by [L8], and hence flat by [F7]; by [L6] the functor $_{i} P \otimes_{A_{m}} -$ is exact on graded left $A_{m}$ -modules. The kernel of the degree-zero surjection $A_{m} \to P_{j}$ , $x \mapsto x e_{j}$ , is the graded submodule $⨁_{k \neq j} P_{k}$ of [F1], so exactness gives an isomorphism $_{i} P \otimes_{A_{m}} P_{j} ≅_{i} P \otimes_{A_{m}} A_{m} / image of_{i} P \otimes_{A_{m}} ⨁_{k \neq j} P_{k}$ ; the unit isomorphism of [L4] identifies $_{i} P \otimes_{A_{m}} A_{m} ≅_{i} P$ by the multiplication map, and the image of the kernel is $_{i} P \cdot ⨁_{k \neq j} P_{k} = \sum_{k \neq j} e_{i} A_{m} e_{k}$ , so $_{i} P \otimes_{A_{m}} P_{j} ≅ e_{i} A_{m} e_{j}$ , the multiplication map $y \otimes x \mapsto y x$ being the isomorphism.

step 1.1L3L4L6L8F7

3.1

Products and orthogonality. By the associativity and unit isomorphisms of [L4] and step 2.1, $U_{i} \otimes_{A_{m}} U_{j} = P_{i} \otimes_{Z}_{i} P \otimes_{A_{m}} P_{j} \otimes_{Z}_{j} P ≅ P_{i} \otimes_{Z} e_{i} A_{m} e_{j} \otimes_{Z}_{j} P,$ with the total-degree grading of [L5], as graded $(A_{m}, A_{m})$ -bimodules. If $∣ i - j ∣ > 1$ then $e_{i} A_{m} e_{j} = 0$ by step 1.1, so $U_{i} \otimes_{A_{m}} U_{j} = 0$ and claim 3 holds.

step 1.1L4L5

4.1

The square relation. Take $j = i$ in step 3.1 and use the basis $e_{i} A_{m} e_{i} = Z e_{i} \oplus Z (i ∣ i - 1 ∣ i)$ of step 1.1, valid because $i \geq 1$ : distributing the tensor over the direct sum, $U_{i} \otimes_{A_{m}} U_{i} ≅ (P_{i} \otimes_{Z} Z e_{i} \otimes_{Z}_{i} P) \oplus (P_{i} \otimes_{Z} Z (i ∣ i - 1 ∣ i) \otimes_{Z}_{i} P)$ . The first summand is $U_{i}$ up to the degree-zero isomorphism $x \otimes e_{i} \otimes y \mapsto x \otimes y$ , since $x e_{i} = x$ for $x \in P_{i}$ ; the second is $U_{i} {1}$ by the shift clause of [L4], because the return $(i ∣ i - 1 ∣ i)$ has degree $1$ by [L3] and $Z (i ∣ i - 1 ∣ i)$ placed in degree $1$ is a shift of the free rank-one module; hence $U_{i} \otimes_{A_{m}} U_{i} ≅ U_{i} \oplus U_{i} {1}$ as graded bimodules, including $i = m$ , where $(m ∣ m - 1 ∣ m)$ is the unique return at $m$ ; applying $- \otimes_{A_{m}} M$ termwise gives the natural isomorphism of functors $U_{i} U_{i} ≅ U_{i} \oplus U_{i} {1}$ .

step 1.1step 3.1L3L4L5

4.2

The triple relations. Apply step 3.1 twice, to $(i, i \pm 1)$ and to $(i \pm 1, i)$ : the $A_{m}$ -pairings have already been consumed by the identifications $_{i} P \otimes_{A_{m}} P_{i \pm 1} ≅ e_{i} A_{m} e_{i \pm 1}$ and $_{i \pm 1} P \otimes_{A_{m}} P_{i} ≅ e_{i \pm 1} A_{m} e_{i}$ of step 2.1, and the remaining pairings are the $Z$ -pairings of the outer factors, so by the associativity of [L4] the triple tensor is $U_{i} \otimes_{A_{m}} U_{i \pm 1} \otimes_{A_{m}} U_{i} ≅ P_{i} \otimes_{Z} (e_{i} A_{m} e_{i \pm 1} \otimes_{Z} e_{i \pm 1} A_{m} e_{i}) \otimes_{Z}_{i} P$ . By step 1.1 the corner $e_{i} A_{m} e_{i + 1} = Z (i ∣ i + 1)$ is free of rank one on a degree-zero element and $e_{i + 1} A_{m} e_{i} = Z (i + 1 ∣ i)$ on a degree-one element, so their tensor over $Z$ is the free rank-one group generated by $(i ∣ i + 1) \otimes (i + 1 ∣ i)$ , which is nonzero because it is the elementary tensor of two basis elements in free rank-one abelian groups; its path product is $(i ∣ i + 1 ∣ i)$ , equal at the interior vertex $i$ , where $0 < i < m$ because $1 \leq i \leq m - 1$ here, to the nonzero basis element $(i ∣ i - 1 ∣ i)$ of $e_{i} A_{m} e_{i}$ of step 1.1; its total degree is $0 + 1 = 1$ . Likewise $e_{i} A_{m} e_{i - 1} = Z (i ∣ i - 1)$ is generated by a degree-one element and $e_{i - 1} A_{m} e_{i} = Z (i - 1 ∣ i)$ by a degree-zero element, so the middle tensor is free of rank one in total degree $1$ in both cases, on the basis element $(i ∣ i - 1 ∣ i)$ of step 1.1 in the second case. Therefore $U_{i} \otimes_{A_{m}} U_{i \pm 1} \otimes_{A_{m}} U_{i} ≅ P_{i} \otimes_{Z} Z {1} \otimes_{Z}_{i} P ≅ U_{i} {1}$ by the shift clause of [L4], and tensoring with $M$ gives the natural isomorphism of functors; the intermediate factor is placed in degree $1$ in both the $i + 1$ and the $i - 1$ case, so the two arrows of the triple contribute total degree $1$ regardless of direction.

step 1.1step 3.1L2L3L4

5.1

Conclusion. The square, triple and orthogonality relations of claims 1 to 3 are steps 4.1, 4.2 and 3.1. Every isomorphism displayed is induced by the identity on the outer factors $P_{i}$ and $_{i} P$ together with the canonical tensor and unit isomorphisms of [L4] and the rank-one degree computations of steps 1.1 and 4.2, so each is a degree-zero bimodule isomorphism natural in the factor that carries the argument module, and each arises from the identity on the path basis; hence $U_{i} U_{i} ≅ U_{i} \oplus U_{i} {1}$ , $U_{i} U_{i \pm 1} U_{i} ≅ U_{i} {1}$ and $U_{i} U_{j} = 0$ for $∣ i - j ∣ > 1$ as natural graded functors. Nothing here compares the two-sided complexes $R_{i}$ and $R_{i + 1}$ , and no braid relation is asserted. The bases used are finite, the shifts are indexed by the finitely many corner paths of step 1.1, and no choice principle is used.

step 1.1step 3.1step 4.1step 4.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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, §2b, printed pp. 11-12 (standard reference, not scraped)