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

• One or more equations did not get rendered due to their size.

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 mem_reesAlgebra_iff_support {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) : f ∈ reesAlgebra I ↔ ∀ i ∈ Polynomial.support f, Polynomial.coeff f 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 : Ideal.FG I) : Subalgebra.FG (reesAlgebra I)

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

Equations

• (_ : Algebra.FiniteType R ↥(reesAlgebra I)) = (_ : Algebra.FiniteType R ↥(reesAlgebra I))

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

Equations

• (_ : IsNoetherianRing ↥(reesAlgebra I)) = (_ : IsNoetherianRing ↥(reesAlgebra I))