I'm reading the paper Noncommutative Gröbner Bases, and Projective Resolutions by Edward L. Green, which presents a version of Buchberger's algorithm for path algebras.
I'm trying to show that the algorithm terminates.
This is the algorithm:
Context: $f_1, \ldots, f_n$ are uniform elements in a path algebra $KQ$, where $Q$ is a (finite) quiver with some admissible order on the set of paths. The paper claims (without proof) that the sequence $\{ g_1, g_2, \ldots \}$ is a Gröbner basis for the ideal $\langle f_1, \ldots, f_n \rangle$.
As an aside, I have some doubts about the correctness of the version of the algorithm presented in the paper. In particular, we need to make the following two modifications to the algorithm:
- We should assume that the input set $\{ f_1, \ldots, f_n \}$ is tip reduced, not just uniform; or we should tip reduce the set before the start of the do-while loop.
- At the end of each iteration of the do-while loop, it is necessary to tip reduce $G$.
(I've found examples that show that both of the modifications described above are necessary, but I'll omit them for now unless someone wants to see them.)
I can see why the algorithm with the above modifications produces a correct result, assuming that it terminates. The paper gives the following argument to show that the algorithm terminates if the ideal $ I = \langle f_1, \ldots, f_n\rangle$ has a finite Gröbner basis:
(Here $I_{MON}$ denotes the ideal $\langle \operatorname{Tip}(I) \rangle$.)
I don't see why the remark preceding the proposition is true. Does anyone know how to prove this remark? Alternatively, does anyone know of a different approach to proving that the algorithm (with the two modifications described earlier) terminates whenever a finite Gröbner basis exists?
One idea I've thought of is to try to prove the following lemma:
Let $$I_1 \subseteq I_2 \subseteq \ldots$$ be a sequence of ideals, all contained in some larger ideal $I$, such that each ideal $I_j$ or $I$ is generated by a finite set of paths. Then there exists some natural number $N$ such that $$I_N = I_{N + 1} = \ldots$$
I'm pretty sure this lemma would imply that the algorithm terminates whenever a finite Gröbner basis exists, although I haven't checked all the details. The problem is that it's not obvious (to me, at least) how one might prove this lemma.
Edit: It's not obvious how one might prove the lemma because the lemma isn't true. For example, suppose that $Q$ is a quiver with one vertex $v$ and two arrows $x$ and $y$. Then $$\langle xyx \rangle \subseteq \langle xyx, xyyx \rangle \subseteq \langle xyx, xyyx, xyyyx \rangle \subseteq \ldots$$ is a sequence of ideals generated by finite sets of paths, all contained in the ideal $\langle v \rangle = KQ$ (or just the ideal $\langle x \rangle$), which is generated by a finite set of paths. But this ascending chain never stabilizes.
Edit 2: I've figured out how to prove the remark preceding proposition 2.8 in Green's paper, which is enough to show that the modified algorithm terminates if a finite Gröbner basis exists. However, the proof of this remark turned out to be pretty long and technical, so I'm not sure if it's feasible to turn it into a self contained answer. I've written down a complete proof as part of my master's thesis, so once my thesis is finished I might post an answer containing a proof sketch and a link to my thesis.