# Documentation

Mathlib.RingTheory.ReesAlgebra

# Rees algebra #

The Rees algebra of an ideal I is the subalgebra R[It] of R[t] defined as R[It] = ⨁ₙ Iⁿ tⁿ. This is used to prove the Artin-Rees lemma, and will potentially enable us to calculate some blowup in the future.

## Main definition #

• reesAlgebra : The Rees algebra of an ideal I, defined as a subalgebra of R[X].
• adjoin_monomial_eq_reesAlgebra : The Rees algebra is generated by the degree one elements.
• reesAlgebra.fg : The Rees algebra of a f.g. ideal is of finite type. In particular, this implies that the rees algebra over a noetherian ring is still noetherian.
def reesAlgebra {R : Type u} [] (I : ) :

The Rees algebra of an ideal I, defined as the subalgebra of R[X] whose i-th coefficient falls in I ^ i.

Instances For
theorem mem_reesAlgebra_iff {R : Type u} [] (I : ) (f : ) :
f ∀ (i : ), I ^ i
theorem mem_reesAlgebra_iff_support {R : Type u} [] (I : ) (f : ) :
f ∀ (i : ), I ^ i
theorem reesAlgebra.monomial_mem {R : Type u} [] {I : } {i : } {r : R} :
↑() r r I ^ i
theorem monomial_mem_adjoin_monomial {R : Type u} [] {I : } {n : } {r : R} (hr : r I ^ n) :
↑() r
theorem adjoin_monomial_eq_reesAlgebra {R : Type u} [] (I : ) :
=
theorem reesAlgebra.fg {R : Type u} [] {I : } (hI : ) :