ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passaudited 2026-10-02

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.

Independent homological and internal shifts on graded K0

Example

Let $k$ be a field, let $A$ be a finite-dimensional unital graded $k$ -algebra and let $P$ be a finite graded projective left $A$ -module, regarded as the bounded complex with $P$ in cohomological degree $0$ and all differentials zero. Then $P [1] {2}$ is a graded perfect complex and its class in $K_{0}^{t r i} (D_{p e r f}^{g r} (A))$ satisfies $[P [1] {2}] = - [P {2}]$ ; identifying that group with $K_{0}^{g r} (A)$ along the graded projective comparison, the same equality reads $[P [1] {2}] = - v^{2} [P],$ and the graded Cartan map carries this class to the element $- v^{2} [P]$ of $G_{0}^{g r} (A)$ . Here $[1]$ is the cochain shift and ${2}$ the internal grading shift: the sign $- 1$ comes from the homological shift and the Laurent factor $v^{2}$ from the internal shift. No finite-global-dimension hypothesis is needed.

Facts & Assumptions

Given: A field $k$ , a finite-dimensional unital graded $k$ -algebra $A$ , and a finite graded projective left $A$ -module $P$ , viewed as the complex with $P$ in cohomological degree $0$ , zero in every other degree, and zero differential.

[F1]

For a graded module $M$ and $r \in Z$ the internal shift $M {r}$ is the graded module with $(M {r})_{d} = M_{d - r}$ carrying the same scalar action; it is invertible with $(M {r}) {- r} = M$ and $M {0} = M$ . On graded complexes the internal shift acts termwise on the terms and leaves every differential unchanged; the cochain shift $[1]$ and the internal shift act on different structures and commute with one another; they need not produce distinct isomorphism classes, since $0 [1] ≅ 0 {1} ≅ 0$ (Associative graded algebras, bimodules, and internal shifts, Perfect complexes over a ring and its graded version).

[F2]

Graded perfect objects are the objects of $D ({GrMod}_{0} (A))$ isomorphic to a bounded complex of finite graded projective left $A$ -modules with degree-zero differentials, and $D_{p e r f}^{g r} (A)$ is an essentially small strictly full triangulated subcategory of $D ({GrMod}_{0} (A))$ (Perfect complexes over a ring and its graded version, Perfect complexes form an essentially small triangulated subcategory).

[F3]

$K_{0}^{t r i} (T)$ of an essentially small triangulated category is the free abelian group on $Iso (T)$ modulo the distinguished-triangle relations $[Y] = [X] + [Z]$ ; in it $[0] = 0$ and $[X [n]] = (- 1)^{n} [X]$ for every integer $n$ (Grothendieck group of an essentially small triangulated category, Shift signs and exact-functor maps on triangulated K0).

[F4]

Degree-zero inclusion induces an isomorphism from the split Grothendieck group of the finite graded projective left $A$ -modules onto $K_{0}^{t r i} (D_{p e r f}^{g r} (A))$ , sending $[Q]$ to $[Q [0]]$ , whose inverse sends the class of a graded perfect object represented by a bounded finite-projective complex $Q$ with degree-zero differentials to $\sum_{n} (- 1)^{n} [Q^{n}]$ (Triangle K0 of perfect complexes equals split K0 of finite projectives).

[F5]

$K_{0}^{g r} (A)$ is the split Grothendieck group of the finite-dimensional graded projective left $A$ -modules and $G_{0}^{g r} (A)$ the Grothendieck group of the finite-dimensional graded left $A$ -modules; both are $Z [v, v^{- 1}]$ -modules with $v^{r} [Q] = [Q {r}]$ and $v^{r} [M] = [M {r}]$ , and the graded Cartan map $c_{A}^{g r} : K_{0}^{g r} (A) \to G_{0}^{g r} (A)$ sends $[Q]$ to $[Q]$ (Graded Grothendieck groups, shift action, and Cartan map).

[F6]

A graded left $A$ -module is finite graded projective if and only if it is a degree-zero direct summand of a finite direct sum of internal shifts $A {r_{1}} \oplus \dots \oplus A {r_{n}}$ (Finite graded projective modules, Finite graded projectives are finite shifted-free summands).

Verification

technique · direct

1.1F1F2F6algebra

By [F6] the module $P$ is a degree-zero direct summand of a finite direct sum $A {r_{1}} \oplus \dots \oplus A {r_{n}}$ ; since $A$ is finite dimensional over $k$ , that sum and hence its summand $P$ are finite dimensional, so $P$ and $P {2}$ are objects of the finite-dimensional graded module category in which $K_{0}^{g r} (A)$ and $G_{0}^{g r} (A)$ are formed. Applying the invertible shift ${2}$ to the splitting exhibits $P {2}$ as a degree-zero direct summand of $A {r_{1} + 2} \oplus \dots \oplus A {r_{n} + 2}$ , so $P {2}$ is again finite graded projective by [F6]. The stalk complex $C$ with $C^{0} = P$ and all other terms and differentials zero is a bounded complex of finite graded projectives with zero, hence degree-zero, differentials, so $C$ and its shifts are objects of $D_{p e r f}^{g r} (A)$ by [F2]. Internal shift acts termwise and does not touch cochain degrees, while the cochain shift does not touch the internal grading, so $C {2} = P {2} [0]$ as complexes, and $C [1] {2} = C {2} [1]$ is the complex with $P {2}$ in cohomological degree $- 1$ and zero differential, i.e. the class $[P [1] {2}]$ is the class of $(P {2}) [1]$ in $K_{0}^{t r i} (D_{p e r f}^{g r} (A))$ .

2.1F2F3step 1.1algebra

Applying the shift-sign identity of [F3] inside the essentially small triangulated category $D_{p e r f}^{g r} (A)$ to the object $X = C {2}$ gives $[X [1]] = - [X]$ , that is $[C {2} [1]] = - [C {2}]$ ; by step 1.1 the left-hand class is $[P [1] {2}]$ and the right-hand class is $- [P {2} [0]]$ , so $[P [1] {2}] = - [P {2} [0]]$ in $K_{0}^{t r i} (D_{p e r f}^{g r} (A))$ .

2.2F4F5step 1.1algebra

In $K_{0}^{g r} (A)$ the shift action gives $v^{2} [P] = [P {2}]$ by [F5], and the graded comparison of [F4] sends this class to $ι_{*} (v^{2} [P]) = [(P {2}) [0]] = [P {2} [0]]$ ; independently, the inverse Euler class of [F4] evaluated on the two-term complex $P [1] {2}$ of step 1.1, whose only nonzero term is $P {2}$ in cohomological degree $- 1$ , equals $(- 1)^{- 1} [P {2}] = - v^{2} [P]$ . Hence $ι_{*} (v^{2} [P]) = [P {2} [0]]$ and $ι_{*}^{- 1} ([P [1] {2}]) = - v^{2} [P]$ .

3.1F4F5step 1.1step 2.1step 2.2algebra∎

Combining steps 2.1 and 2.2, $[P [1] {2}] = - [P {2} [0]] = - ι_{*} (v^{2} [P])$ ; that is, identifying $K_{0}^{t r i} (D_{p e r f}^{g r} (A))$ with $K_{0}^{g r} (A)$ along the comparison isomorphism $ι_{*}$ of [F4], the class of the homological-and-internal shift of the degree-zero complex is $[P [1] {2}] = - v^{2} [P]$ , the sign coming from $[1]$ and the factor $v^{2}$ from ${2}$ . Since the Cartan map of [F5] sends $[Q] \mapsto [Q]$ and both $K_{0}^{g r} (A)$ and $G_{0}^{g r} (A)$ have $v$ acting by internal shift, $c_{A}^{g r} (- v^{2} [P]) = - v^{2} [P]$ , so the image of $[P [1] {2}]$ in $G_{0}^{g r} (A)$ obeys the same formula $- v^{2} [P]$ . The differentials of $P [1] {2}$ vanish identically because $P$ sits in a single cohomological degree, so the internal shift introduces no cochain sign; only the homological shift contributes the sign $- 1$ , and no finite-global-dimension or Noetherian hypothesis is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

Khovanov and Seidel, Quivers, Floer Cohomology, and Braid Group Actions, §§2c and 2e.1 (standard reference, not scraped)