/-!

​

# Hilbert basis theorem

​

All rings are commutative and have a 1; all morphisms of rings send 1 to 1.

​

A commutative ring is said to be *Noetherian* if all ideals

are finitely generated. This turns out to be an extremely

important finiteness condition for rings. It is named after

the German mathematician Emmy Noether.

​

The Hilbert Basis Theorem says that if `R` is

a Noetherian ring, then so is the ring `R[X]` of polynomials

in one variable over `R`. Here is how to state the Hilbert

basis theorem in Lean:

​

```lean

theorem Hilbert_Basis_Theorem 

  (R : Type) [comm_ring R] (hR : is_noetherian_ring R) :

  is_noetherian_ring (polynomial R) := ...

```

​

Here's a paper proof.

​

We start with a definition. For R a ring and n a natural number, let Mₙ denote the polynomials in R[X] of

degree at most n. It's clearly an R-submodule, and if j is a natural number then projection prⱼ onto the coefficient

of Xᶨ is an R-module homomorphism R[X] → R and hence Mₙ → R.

 Assume R is a Noetherian ring and let I be an ideal of R[X]. We want

 to prove that I is finitely-generated.

​

  Define J_n to be the ideal prₙ (Mₙ ∩ I)

  Clearly the J_n are an increasing sequence of ideals (use multiplication by X).

  Let J be their union.

​

    J is a finitely generated R-mod, generated by {j₁, j₂,…jₙ}

    choose hᵢ ∈ I representing jᵢ

    Let N be max of the degrees of the hᵢ, so J=J_N.

    Now here is a finite set S of generators for I.

    It's the obviously finite union of the following things

    * h's corresponding to generators of

    all the J_n for n ≤ N.

    * The hᵢ from above 

    Proof:

    Say f is in J

    By strong Induction on deg(f) it suffices to prove that for 

    every non-zero poly f in I, there exists g in the ideal (S)

    such that f-g has smaller degree than f

    So say f is non-zero. Two cases.

    1) deg(f) = d ≤ N

    Then the h's corresponding to J_d will do the job.

    2) deg(f) =d > N

    Then the leading coefficient of f is in J=J_N

    and we can use X^{d-N} 

-/