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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯