# mathlibdocumentation

ring_theory.rees_algebra

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

• rees_algebra : The Rees algebra of an ideal I, defined as a subalgebra of R[X].
• adjoin_monomial_eq_rees_algebra : The Rees algebra is generated by the degree one elements.
• rees_algebra.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 rees_algebra {R : Type u} [comm_ring R] (I : ideal R) :

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

Equations
Instances for ↥rees_algebra
theorem mem_rees_algebra_iff {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :
∀ (i : ), f.coeff i I ^ i
theorem mem_rees_algebra_iff_support {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :
∀ (i : ), i f.supportf.coeff i I ^ i
theorem rees_algebra.monomial_mem {R : Type u} [comm_ring R] {I : ideal R} {i : } {r : R} :
r I ^ i
theorem monomial_mem_adjoin_monomial {R : Type u} [comm_ring R] {I : ideal R} {n : } {r : R} (hr : r I ^ n) :
r
theorem adjoin_monomial_eq_rees_algebra {R : Type u} [comm_ring R] (I : ideal R) :
theorem rees_algebra.fg {R : Type u} [comm_ring R] {I : ideal R} (hI : I.fg) :
@[protected, instance]
def rees_algebra.algebra.finite_type {R : Type u} [comm_ring R] {I : ideal R}  :
@[protected, instance]
def rees_algebra.is_noetherian_ring {R : Type u} [comm_ring R] {I : ideal R}  :