Rees algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

def rees_algebra {R : Type u} [comm_ring R] (I : ideal R) :

subalgebra R (polynomial R)

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

Equations

rees_algebra I = {carrier := {f : polynomial R | ∀ (i : ℕ), f.coeff i ∈ I ^ i}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}

Instances for ↥rees_algebra

source

theorem mem_rees_algebra_iff {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

f ∈ rees_algebra I ↔ ∀ (i : ℕ), f.coeff i ∈ I ^ i

source

theorem mem_rees_algebra_iff_support {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

f ∈ rees_algebra I ↔ ∀ (i : ℕ), i ∈ f.support → f.coeff i ∈ I ^ i

source

theorem rees_algebra.monomial_mem {R : Type u} [comm_ring R] {I : ideal R} {i : ℕ} {r : R} :

⇑(polynomial.monomial i) r ∈ rees_algebra I ↔ r ∈ I ^ i

source

theorem monomial_mem_adjoin_monomial {R : Type u} [comm_ring R] {I : ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) :

⇑(polynomial.monomial n) r ∈ algebra.adjoin R ↑(submodule.map (polynomial.monomial 1) I)

source

theorem adjoin_monomial_eq_rees_algebra {R : Type u} [comm_ring R] (I : ideal R) :

algebra.adjoin R ↑(submodule.map (polynomial.monomial 1) I) = rees_algebra I

source

theorem rees_algebra.fg {R : Type u} [comm_ring R] {I : ideal R} (hI : I.fg) :

(rees_algebra I).fg

source

@[protected, instance]

def rees_algebra.algebra.finite_type {R : Type u} [comm_ring R] {I : ideal R} [is_noetherian_ring R] :

algebra.finite_type R ↥(rees_algebra I)

source

@[protected, instance]

def rees_algebra.is_noetherian_ring {R : Type u} [comm_ring R] {I : ideal R} [is_noetherian_ring R] :

is_noetherian_ring ↥(rees_algebra I)