noncomputable def GradedRingQuotient.reesIdealFromBase {A : Type u} [CommRing A] (I : Ideal A) : Ideal ↥(reesAlgebra I)

Ideal of the Rees algebra generated by the image of I ⊆ A.

def GradedRingQuotient.assocGradedRing {A : Type u} [CommRing A] (I : Ideal A) : Type u

Associated graded ring gr_I(A) = ⊕_p I^p / I^{p+1} realized via the Rees algebra.

@[implicit_reducible]

noncomputable instance GradedRingQuotient.assocGradedRing.commRing {A : Type u} [CommRing A] (I : Ideal A) : CommRing (assocGradedRing I)

The associated graded ring is a commutative ring.

theorem GradedRingQuotient.monomial_mem_reesAlgebra {A : Type u} [CommRing A] (I : Ideal A) (p : ℕ) (a : A) (ha : a ∈ I ^ p) : (Polynomial.monomial p) a ∈ reesAlgebra I

If a ∈ I^p, then the monomial a · t^p belongs to the Rees algebra of I.

noncomputable def GradedRingQuotient.imageInAssocGraded {A : Type u} [CommRing A] (I : Ideal A) (p : ℕ) (a : A) (ha : a ∈ I ^ p) : assocGradedRing I

Image in gr_I(A) of an element a ∈ I^p, viewed as a degree-p homogeneous element.

noncomputable def GradedRingQuotient.quotientIdeal {A : Type u} [CommRing A] (𝔪 : Ideal A) (a : A) : Ideal (A ⧸ Ideal.span {a})

Image of the ideal 𝔪 under the quotient map A → A / (a).

theorem GradedRingQuotient.lemma_32_graded_ring_quotient {A : Type u} [CommRing A] (𝔪 : Ideal A) [𝔪.IsMaximal] (a : A) (p : ℕ) (ha : a ∈ 𝔪 ^ p) (hreg : imageInAssocGraded 𝔪 p a ha ∈ nonZeroDivisors (assocGradedRing 𝔪)) : Nonempty (assocGradedRing (quotientIdeal 𝔪 a) ≃+* assocGradedRing 𝔪 ⧸ Ideal.span {imageInAssocGraded 𝔪 p a ha})

Lemma 32: if a ∈ 𝔪^p and its image in gr_𝔪(A) is a nonzero divisor, then gr_{𝔪/(a)}(A/(a)) ≃ gr_𝔪(A) / (image of a).