LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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 graded horseshoe lemma for finite graded projective resolutions

Statement

Fix $m \geq 1$ and let $A_{m} -mod$ be the abelian category of finite generated graded left $A_{m}$ -modules and degree-zero maps of Finite graded A_m-modules, internal shifts and the vertex projectives. Let $0 \to M^{'} \overset{i}{\to} M \overset{q}{\to} M^{''} \to 0$ be degreewise exact in $A_{m} -mod$ , so that $i$ is injective, $q$ is surjective and $im i = \ker q$ degreewise, and suppose that $M^{'}$ admits a finite graded projective resolution of length at most $a$ and $M^{''}$ one of length at most $b$ , in the sense that the resolutions $0 \to P_{a}^{'} \to \dots \to P_{1}^{'} \to P_{0}^{'} \overset{ε^{'}}{\to} M^{'} \to 0, 0 \to P_{b}^{''} \to \dots \to P_{1}^{''} \to P_{0}^{''} \overset{ε^{''}}{\to} M^{''} \to 0$ consist of finitely generated graded projective modules with $P_{n}^{'} = 0$ for $n > a$ and $P_{n}^{''} = 0$ for $n > b$ . Then $M$ admits a finite graded projective resolution of length at most $\max (a, b)$ , that is, there is an exact sequence $0 \to P_{\max (a, b)} \to \dots \to P_{1} \to P_{0} \overset{ε}{\to} M \to 0$ of finitely generated graded projectives with $P_{n} = 0$ for $n > \max (a, b)$ .

In particular, writing $pd$ for the least such length (so that $pd X = 0$ exactly when $X$ is finite graded projective, and the zero module has $pd 0 = 0$ ), every degreewise extension of two objects of finite projective dimension has finite projective dimension with $pd M \leq \max (pd M^{'}, pd M^{''})$ . The argument is a horseshoe construction carried out on elements of graded modules and selects only finitely many lifts; it uses no choice principle and no arbitrary-abelian-category element chase.

Facts & Assumptions

Given: An integer $m \geq 1$ , the abelian category $A_{m} -mod$ over the algebra $A_{m}$ , and a degreewise short exact sequence $0 \to M^{'} \to M \to M^{''} \to 0$ in it.

[L1]

$A_{m} -mod$ is the abelian category of finitely generated graded left $A_{m}$ -modules and degree-zero maps; kernels, cokernels and finite biproducts are computed degreewise and a sequence is exact precisely when it is exact degreewise; each vertex projective $P_{i} = A_{m} e_{i}$ is a finite graded projective left $A_{m}$ -module (Finite graded A_m-modules, internal shifts and the vertex projectives).

[L2]

$A_{m}$ is free of rank $4 m + 1$ as a graded abelian group with basis the $4 m + 1$ displayed vertex, arrow and return classes, so its underlying $Z$ -module is free of finite rank $4 m + 1$ (The 4m+1 path basis).

[F3]

Every principal ideal domain is Noetherian; $Z$ is a principal ideal domain (Every principal ideal domain is Noetherian).

[L4]

Every finitely generated left module over a left Noetherian ring is Noetherian (Finitely generated modules over a left Noetherian ring are Noetherian).

[F5]

A unital ring $R$ is left Noetherian when its left regular module $_{R} R$ is Noetherian, and unqualified "Noetherian ring" means left Noetherian (Left and right Noetherian rings).

[L6]

A left $R$ -module $M$ is Noetherian when every submodule of $M$ is finitely generated (Noetherian modules: every submodule is finitely generated).

[F7]

A graded left $A_{m}$ -module $P$ is graded projective when every degree-zero epimorphism $q : E ↠ M$ and every degree-zero $f : P \to M$ admit a degree-zero lift $\tilde{f} : P \to E$ with $q \tilde{f} = f$ , and $P$ is finite graded projective when in addition it is generated by finitely many homogeneous elements; the zero module is finite graded projective (Finite graded projective modules).

[L8]

A graded left $A$ -module $P$ 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 projectives are finite shifted-free summands).

[F9]

A projective resolution of an object $X$ of an abelian category is an augmented chain complex $\dots \to P_{1} \to P_{0} \overset{ε}{\to} X \to 0$ with every $P_{n}$ projective that is exact at every displayed term (Projective resolutions in an abelian category).

[F10]

For an $A_{m}$ -linear degree-zero map $f : X \to Y$ of graded left $A_{m}$ -modules, the kernel and the image are graded submodules of $X$ and $Y$ and are computed degreewise; a map is a monomorphism exactly when it is injective and an epimorphism exactly when it is surjective (Graded modules with degree-zero maps form an abelian category).

Proof

technique · direct

1.1

$A_{m}$ is left Noetherian. By [L2] the underlying $Z$ -module of $A_{m}$ is free of finite rank, hence finitely generated, and $Z$ is Noetherian by [F3]; so $A_{m}$ is a Noetherian $Z$ -module by [L4], which by [L6] means that every $Z$ -submodule of $A_{m}$ is finitely generated as a $Z$ -module. A left ideal of $A_{m}$ is a $Z$ -submodule, so every left ideal is finitely generated as a $Z$ -module and hence as a left ideal; since the submodules of the left regular module $_{A} A_{m}$ are exactly the left ideals, the regular module is Noetherian and [F5] makes $A_{m}$ left Noetherian.

L2F3L4F5L6

1.2

The lift and the comparison map $φ$ . For the augmentation $ε^{''} : P_{0}^{''} \to M^{''}$ of [F9] and the epimorphism $q : M \to M^{''}$ , the module $P_{0}^{''}$ is finite graded projective and $q$ is a degree-zero epimorphism, so the lifting property of [F7] produces a degree-zero $g : P_{0}^{''} \to M$ with $q g = ε^{''}$ . Let $φ : P_{0}^{'} \oplus P_{0}^{''} \to M$ be the degree-zero map $φ (x^{'}, x^{''}) : = i ε^{'} (x^{'}) + g (x^{''})$ ; both summands lie in $M$ , and $φ$ is $A_{m}$ -linear because $i$ , $ε^{'}$ and $g$ are.

F7F9

1.3

Projectivity of the prepended term. The direct sum $P_{0}^{'} \oplus P_{0}^{''}$ is a finite graded projective left $A_{m}$ -module: by [L8] the modules $P_{0}^{'}$ and $P_{0}^{''}$ are degree-zero direct summands of finite direct sums of shifts of $A_{m}$ , and the direct sum of two such summands, with the summand inclusions and projections added componentwise, is a degree-zero direct summand of the direct sum of the two finite direct sums of shifts, which is again a finite direct sum of shifts of $A_{m}$ ; so [L8] applies to $P_{0}^{'} \oplus P_{0}^{''}$ .

L8F7

1.4

The horseshoe recursion. We prove by induction on $N \geq 0$ the statement $P (N)$ : for every degreewise short exact sequence $0 \to M^{'} \to M \to M^{''} \to 0$ in $A_{m} -mod$ and all integers $a, b \geq 0$ with $\max (a, b) \leq N$ such that $M^{'}$ has a finite graded projective resolution of length at most $a$ and $M^{''}$ one of length at most $b$ , the module $M$ has a finite graded projective resolution of length at most $\max (a, b)$ .

2.1

Submodules of finitely generated graded modules are finitely generated. Let $N$ be a finitely generated graded left $A_{m}$ -module and $S \leq N$ a submodule. Then $N$ is a finitely generated left module over the left Noetherian ring $A_{m}$ of step 1.1, so [L4] makes $N$ Noetherian, and by [L6] the submodule $S$ is finitely generated over $A_{m}$ . Applied to $S$ a graded submodule, this gives a finite $A_{m}$ -generating family of $S$ , which by the homogeneous-component rewriting recorded in [F7] may be taken homogeneous; in particular the kernel of any degree-zero map of finitely generated graded left $A_{m}$ -modules is again an object of $A_{m} -mod$ .

step 1.1L4L6F7

2.2

$φ$ is an epimorphism. Let $m \in M$ . Since $ε^{''} : P_{0}^{''} \to M^{''}$ is surjective by [F9], there is $x^{''} \in P_{0}^{''}$ with $q (m) = ε^{''} (x^{''}) = q g (x^{''})$ ; then $m - g (x^{''}) \in \ker q = im i$ , so $m - g (x^{''}) = i (m^{'})$ for some $m^{'} \in M^{'}$ , and surjectivity of $ε^{'}$ gives $x^{'} \in P_{0}^{'}$ with $ε^{'} (x^{'}) = m^{'}$ . Thus $φ (x^{'}, x^{''}) = i ε^{'} (x^{'}) + g (x^{''}) = i (m^{'}) + g (x^{''}) = m$ , so $φ$ is surjective and hence an epimorphism by [F10].

step 1.2F9F10

3.1

The kernel stays finitely generated. Let $K : = \ker φ \leq P_{0}^{'} \oplus P_{0}^{''}$ . The module $P_{0}^{'}$ is finite graded projective, in particular finitely generated, and so is $P_{0}^{''}$ ; hence $P_{0}^{'} \oplus P_{0}^{''}$ is finitely generated as a graded left $A_{m}$ -module, and by step 2.1 the submodule $K$ is finitely generated, so $K$ is an object of $A_{m} -mod$ .

step 2.1F7

4.1

The syzygy sequence is degreewise short exact. Put $K^{'} : = \ker ε^{'} \leq P_{0}^{'}$ and $K^{''} : = \ker ε^{''} \leq P_{0}^{''}$ . The projection $π : K \to K^{''}$ , $(x^{'}, x^{''}) \mapsto x^{''}$ , lands in $K^{''}$ : if $φ (x^{'}, x^{''}) = i ε^{'} (x^{'}) + g (x^{''}) = 0$ , then $ε^{''} (x^{''}) = q g (x^{''}) = - q i ε^{'} (x^{'}) = 0$ . The inclusion $ȷ : K^{'} \to K$ , $x^{'} \mapsto (x^{'}, 0)$ , has image exactly $\ker π$ , since $(x^{'}, 0) \in K$ means $i ε^{'} (x^{'}) = 0$ , equivalently $ε^{'} (x^{'}) = 0$ because $i$ is injective. The map $π$ is surjective: given $x^{''} \in K^{''}$ , one has $q g (x^{''}) = ε^{''} (x^{''}) = 0$ , so $g (x^{''}) = i (m^{'})$ for some $m^{'} \in M^{'}$ ; choose $x^{'} \in P_{0}^{'}$ with $ε^{'} (x^{'}) = - m^{'}$ , possible because $ε^{'}$ is surjective. Then $φ (x^{'}, x^{''}) = - i (m^{'}) + g (x^{''}) = 0$ , and $(x^{'}, x^{''}) \in K$ maps to $x^{''}$ . These are degree-zero module maps, and [L1] makes $0 \to K^{'} \overset{ȷ}{\to} K \overset{π}{\to} K^{''} \to 0$ degreewise exact in $A_{m} -mod$ ; $K, K^{'}, K^{''}$ are finite graded modules by step 3.1 and step 2.1.

step 2.1step 3.1L1F10

Base case $N = 0$ . Here $a = b = 0$ , so the resolutions $0 \to P_{0}^{'} \overset{ε^{'}}{\to} M^{'} \to 0$ and $0 \to P_{0}^{''} \overset{ε^{''}}{\to} M^{''} \to 0$ are exact, so $ε^{'}$ and $ε^{''}$ are isomorphisms and $K^{'} = K^{''} = 0$ . By step 4.1 the sequence $0 \to 0 \to K \to 0 \to 0$ is degreewise exact, so $K = 0$ ; by steps 1.2 and 2.2 the map $φ : P_{0}^{'} \oplus P_{0}^{''} \to M$ is an epimorphism with zero kernel, hence an isomorphism by [F10], and $M$ is finite graded projective by step 1.3. So $0 \to P_{0}^{'} \oplus P_{0}^{''} \overset{φ}{\to} M \to 0$ is a finite graded projective resolution of $M$ of length $0 = \max (a, b)$ , and $P (0)$ holds.

Inductive step. Assume $N \geq 1$ and $P (N - 1)$ , and let $a, b$ with $c : = \max (a, b) \leq N$ be given. If $c = 0$ , the base-case argument already proves the claim. Suppose $c \geq 1$ . If $a \geq 1$ , set $a^{*} : = a - 1$ ; if $a = 0$ , set $a^{*} : = 0$ . Then $a^{*} \leq N - 1$ in both cases, because $a \geq 1$ gives $a - 1 \leq N - 1$ and $a = 0$ gives $a^{*} = 0 \leq N - 1$ as $N \geq 1$ . Define $b^{*}$ from $b$ in the same way, so $b^{*} \leq N - 1$ as well. First syzygies have resolutions of these lengths: if $a \geq 1$ , the exactness of the resolution of [F9] at $P_{1}^{'}, \dots, P_{a - 1}^{'}$ and the vanishing $P_{a + 1}^{'} = 0$ show that $0 \to P_{a}^{'} \to \dots \to P_{1}^{'} \to K^{'} \to 0$ is a finite graded projective resolution of $K^{'}$ of length $a - 1 = a^{*}$ ; if $a = 0$ , then $K^{'} = 0$ and the zero complex $0 \to 0 \to K^{'} \to 0$ is a finite graded projective resolution of $K^{'}$ of length $0 = a^{*}$ , the zero module being finite graded projective by [F7]; the same alternative holds for $K^{''}$ with $b^{*}$ . By step 4.1 the sequence $0 \to K^{'} \to K \to K^{''} \to 0$ is degreewise short exact in $A_{m} -mod$ , so $P (N - 1)$ applies to it with the bounds $a^{*}, b^{*}$ and yields a finite graded projective resolution of $K$ of length at most $\max (a^{*}, b^{*}) = c - 1 \leq N - 1$ . Prepending the epimorphism $φ : P_{0}^{'} \oplus P_{0}^{''} \to M$ of step 1.2, with kernel $K$ the finitely generated module of step 3.1, produces $0 \to \dots \to P_{0} \overset{φ}{\to} M \to 0$ with $P_{0} : = P_{0}^{'} \oplus P_{0}^{''}$ finite graded projective by step 1.3 and all higher terms those of the resolution of $K$ , so $M$ has a finite graded projective resolution of length at most $\max (a^{*}, b^{*}) + 1 = c = \max (a, b) \leq N$ , and $P (N)$ holds.

Every step of the recursion is a single application of the lifting property of [F7] and finitely many element choices inside a fixed module, and the induction hypothesis is applied to finitely many sequences; no family indexed by an infinite set is selected. [step 1.2, step 2.2, step 3.1, step 4.1, step 1.3, F7, F9, F10]

5.1

Conclusion. Applying $P (N)$ of step 1.4 with $N : = \max (a, b)$ proves the first claim: a degreewise short exact sequence $0 \to M^{'} \to M \to M^{''} \to 0$ in $A_{m} -mod$ whose outer terms carry finite graded projective resolutions of lengths at most $a$ and $b$ makes $M$ carry one of length at most $\max (a, b)$ ; taking $a = pd M^{'}$ and $b = pd M^{''}$ gives $pd M \leq \max (pd M^{'}, pd M^{''})$ , and the construction never selects more than finitely many lifts, so no choice principle is used.

step 1.4F7∎

Depends on

Used by

Finite homological dimension of the finite graded Khovanov-Seidel module category Theorem

Dependency tree · two levels

36 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

Charles Weibel, An Introduction to Homological Algebra, ch. 2 §2.2, pp. 36-38 (standard reference, not scraped)
Mikhail Khovanov and Paul Seidel, Quivers, Floer Cohomology, and Braid Group Actions, §2a, printed pp. 9-11 (standard reference, not scraped)