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} [CommRing 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

• reesAlgebra I = { carrier := {f : Polynomial R | ∀ (i : ℕ), f.coeff i ∈ I ^ i}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

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 ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i

theorem reesAlgebra.monomial_mem {R : Type u} [CommRing R] {I : Ideal R} {i : ℕ} {r : R} : (Polynomial.monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i

theorem reesAlgebra.monomial_coeff_mem {R : Type u} [CommRing R] {I : Ideal R} (f : ↥(reesAlgebra I)) (i : ℕ) : (Polynomial.monomial i) ((↑f).coeff i) ∈ reesAlgebra I

theorem reesAlgebra.as_sum_support {R : Type u} [CommRing R] {I : Ideal R} (f : ↥(reesAlgebra I)) : f = ∑ i ∈ (↑f).support, ⟨(Polynomial.monomial i) ((↑f).coeff i), ⋯⟩

theorem monomial_mem_adjoin_monomial {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) : (Polynomial.monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I)

theorem adjoin_monomial_eq_reesAlgebra {R : Type u} [CommRing R] (I : Ideal R) : Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I) = reesAlgebra I

theorem reesAlgebra.fg {R : Type u} [CommRing R] {I : Ideal R} (hI : I.FG) : (reesAlgebra I).FG

instance instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing {R : Type u} [CommRing R] {I : Ideal R} [IsNoetherianRing R] : Algebra.FiniteType R ↥(reesAlgebra I)

instance instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra {R : Type u} [CommRing R] {I : Ideal R} [IsNoetherianRing R] : IsNoetherianRing ↥(reesAlgebra I)

theorem tensorProduct_reesAlgebra_isNoetherian_of_fg {R : Type u} [CommRing R] {I : Ideal R} [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : IsNoetherianRing (TensorProduct R (R ⧸ I) ↥(reesAlgebra I))

theorem isNoetherianRing_reesAlgebra_quotient {R : Type u} [CommRing R] {I : Ideal R} [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : IsNoetherianRing (↥(reesAlgebra I) ⧸ Ideal.map (algebraMap R ↥(reesAlgebra I)) I)

theorem mem_map_algebraMap_reesAlgebra_iff {R : Type u} [CommRing R] {I : Ideal R} (f : ↥(reesAlgebra I)) : f ∈ Ideal.map (algebraMap R ↥(reesAlgebra I)) I ↔ ∀ (n : ℕ), (↑f).coeff n ∈ I ^ (n + 1)