# 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.

Equations
• = { carrier := {f : | ∀ (i : ), f.coeff i I ^ i}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
Instances For
theorem mem_reesAlgebra_iff {R : Type u} [] (I : ) (f : ) :
f ∀ (i : ), f.coeff i I ^ i
theorem mem_reesAlgebra_iff_support {R : Type u} [] (I : ) (f : ) :
f if.support, f.coeff 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 : I.FG) :
().FG
Equations
• =