Trying to understand basic Gröbner basis theorem

Question

The following is from some study material I was provided. I will interject at the parts that have stumped me.

Theorem

Let < be a monomial order on the polynomial ring K[X].
Let ⟨0⟩ ≠ I ⊂ K[X] be an ideal.
Let {g₁, g₂, ..., g_s} be the Gröbner basis of I with respect to <.

Then:

I = ⟨g₁, g₂, ..., g_s⟩.

Proof

By assumption, {g₁, g₂, ..., g_s} is the Gröbner basis of I with respect to <.

Hence one has:

⟨in_<(g₁), in_<(g₂), ..., in_<(g₂)⟩ = in_<(I).

Now we prove I = ⟨g₁, g₂, ..., g_s⟩.
In general, ⟨g₁, g₂, ..., g_s⟩ ⊂ I holds since g₁, g₂, ..., g_s ∈ I. Hence it is enough to show that I ⊂ ⟨g₁, g₂, ..., g_s⟩.

Let 0 ≠ f ∈ I be a polynomial.
Then in_<(f) ∈ in_<(I).
Hence there exists an integer 1 ≦ i ≦ s and a monomial w such that in_<(f) = w・in_<(g_i).
Then in_<(f) = in_<(wg_i) by virtue of [lemma discussed earlier in the study material].
The initial term of f is of the form c・in_< and the initial term of wg_i is of the form c_i・in_<(wg_i), where 0 ≠ c, c_i ∈ K.

Now we let

f⁽¹⁾ := c_i・f - c・wg_i.

Then one has f⁽¹⁾ ∈ I since I is an ideal and f, g_i ⊂ ⟨g₁, g₂, ..., g_s⟩ ∈ I.
Moreover, if f⁽¹⁾ = 0, then f = (c/c_iwg_i ∈ ⟨g_i⟩ ⊂ ⟨g₁, g₂, ..., g_s⟩ and I ⊂ ⟨g₁, g₂, ..., g_s⟩.

My first problem

I can't quite follow the last step. How does proving that one element f of I is also an element of the ideal ⟨g₁, g₂, ..., g_s⟩ prove that all elements of the I are contained in ⟨g₁, g₂, ..., g_s⟩?

Back to the proof

Assume that f⁽¹⁾ ≠ 0.
Then one has in_<(f⁽¹⁾) < in_<(f) and we can take a polynomial f⁽²⁾ ∈ I by using the same technique as we used for making f⁽¹⁾.
If f⁽²⁾ = 0, then f⁽¹⁾ ∈ ⟨g₁, g₂, ..., g_s⟩ and f ∈ ⟨g₁, g₂, ..., g_s⟩.

Assume that f⁽²⁾ ≠ 0.
Then one has in_<(f⁽²⁾) < in_<(f⁽¹⁾).
In general, in the case that f^(k-1) ≠ 0, then we can take a polynomial f^(k) ∈ I by using the same technique as we used for making f^(k-1).
If f^(k) = 0, then f⁽¹⁾, f⁽²⁾, ..., f^(k) ∈ ⟨g₁, g₂, ..., g_s⟩.

Hence one has f ∈ ⟨g₁, g₂, ..., g_s⟩.
Thus it is enough to show that there exists an integer k ≧ 1 such that f^(k) = 0.

Suppose that f^(k) ≠ 0 for all k ≧ 1.
Then the infinite sequence of monomials

in_<(f) > in_<(f⁽¹⁾) > ... > in_<(f^(k)) > ...

arises. However, this contradicts the statement of [another lemma discussed outside of this text].
Therefore it follows that there exists an integer k ≧ 1 such that _f^(k) = 0.

My second problem

How exactly are f⁽²⁾ onwards defined? Is it like f⁽²⁾ := c_i・f⁽¹⁾ - c・wg_i, in which the parameters c, i, and w are all the same as for f⁽¹⁾?

Answer 1

1. Note that $f$ was taken to be an arbitrary (nonzero) element of $I$ (= every element of $I$ can be taken). Proving set inclusion $A \subset B$ amounts to showing that every element of $A$ also lies in $B$. Zero is in $I$ by definition.

2. One takes the initial term $T_1$ of $f^{(1)}$ and finds an element $g_i$ of the Groebner basis with an initial term $T_1'$ that divides $T_1$. Then one multiplies $g_i$ by a certain monomial $m_i$ and a coefficient $\alpha_i$ so the result's initial term is exactly equal to $T_1$. Then $f^{(2)} = f^{(1)} - \alpha_i m_i g_i$ only contains terms that are strictly smaller than $T_1$.