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
  • reesAlgebra I = { carrier := {f : Polynomial R | ∀ (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} [CommRing R] (I : Ideal R) (f : Polynomial R) :
    f reesAlgebra I ∀ (i : ), f.coeff i I ^ i
    theorem mem_reesAlgebra_iff_support {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) :
    f reesAlgebra I if.support, f.coeff 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 : I.FG) :