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 #

def reesAlgebra {R : Type u} [CommRing 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
  • One or more equations did not get rendered due to their size.
Instances For
    theorem mem_reesAlgebra_iff {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) :
    f reesAlgebra I ∀ (i : ), Polynomial.coeff f i I ^ i
    theorem reesAlgebra.monomial_mem {R : Type u} [CommRing R] {I : Ideal R} {i : } {r : R} :
    theorem monomial_mem_adjoin_monomial {R : Type u} [CommRing R] {I : Ideal R} {n : } {r : R} (hr : r I ^ n) :
    theorem reesAlgebra.fg {R : Type u} [CommRing R] {I : Ideal R} (hI : Ideal.FG I) :