Let $F$ be a free module (of finite rank) over $S = k[x_1, \dots , x_r]$ with monomial order >. Let $M \subset F$ be a submodule and let $B = \{g_1, \dots , g_t\}$ be a Gröbner basis for $M.$
I found the following idea used alot: if $\operatorname{in}(M)$ is generated by $\operatorname{in}(g_1), \dots ,\operatorname{in}(g_s)$ for some $s \leq t,$ then $\{g_1, \dots , g_s\}$ is also a Gröbner basis for $M.$
My previous knowledge is (From Eisenbud "Commutative algebra, with a view toward algebraic geometry" pg.328 and pg. 325):
If $>$ is a monomial order, then for any $f \in F$ we define the initial term of $f,$ written $in_{>}(f)$ to be the greatest term of $f$ with respect to the order $>,$ and if $M$ is a submodule of $F$ we define $in_{>}(M)$ to be the monomial submodule generated by the elements $in_{>}(f)$ for all $f \in M.$
A Gröbner basis with respect to an order $>$ on a free module with basis $F$ is a set of elements $g_1, \dots , g_t \in F$ such that if $M$ is the submodule of $F$ generated by $g_1, \dots , g_t,$ then $in_{>}(g_1), \dots , in_{>}(g_t)$ generate $in_{>}(M).$
My idea of the solution:
My intuition is that this follows directly from the definition of Gröbner basis but I want to write this in a succinct way, is there any suggestions for a proof? I want to straighten this proof out, please.
Thanks in advance!
Ok, here is the proof. We only follow the definition and the division algorithm.
To show that $\{g_1, \dots , g_s\}$ is a Groebner basis for $M$ we have to show two things in general:
1/ $\{g_1, \dots , g_s\}$ is a generating set for $M$ (as $S-$ module), i.e, for every $f\in M$, there exist $f_1,\ldots ,f_s \in S$ such that $$f=f_1g_1+\ldots f_sg_s$$
2/ $\operatorname{in}(g_1), \dots ,\operatorname{in}(g_s)$ is a generating set for $\operatorname{in}(M)$ (as $S-$ module).
By the assumption, we have already have $2/$ so we only need to prove $1/$.
Now, by division algorithm (prop 15.6 in Eisenbud's book), for any $f\in M$, there exist $f_1,\ldots ,f_s \in S$ and $f'\in F$ such that $$f=f_1g_1+\ldots f_sg_s +f'$$ where none of the monomials in $f'$ is in $(\operatorname{in}(g_1), \dots ,\operatorname{in}(g_s)) =\operatorname{in}(M)$. However, since
$$f'=f-(f_1g_1+\ldots f_sg_s) \in M$$ we have that $\operatorname{in}(f') \in \operatorname{in}(M)$, which is a contradiction (because $\operatorname{in}(f')$ is a monomial of $f'$). Therefore, $f'=0$, hence the claim.