The grading of the Rees algebra

Mathlib realizes the Rees algebra R[It] = ⨁ₙ Iⁿ tⁿ of an ideal I of a commutative ring R as the subalgebra reesAlgebra I of R[X] of polynomials whose n-th coefficient lies in Iⁿ, so that t is the variable X. This file equips it with its grading by the power of X: the degree n piece reesAlgebra.grade I n consists of the monomials r Xⁿ with r ∈ Iⁿ, and the homogeneous components of an element are its monomials. The degree zero piece is a copy of R, and the irrelevant ideal is generated in degree one by the elements a t with a running over generators of I.

With this grading, Proj of the Rees algebra is the blowup of Spec R along V(I); the last fact says that it is covered by the standard opens D₊(a t).

Main definitions

• reesAlgebra.grade I n: the degree n piece of the Rees algebra.
• reesAlgebra.gradedAlgebra: the GradedAlgebra instance on reesAlgebra I.
• reesAlgebra.gradeZeroEquiv: the degree zero piece is isomorphic to R.
• reesAlgebra.monomialDegreeOne ha: the element a t of degree one, for a ∈ I.

Main results

• reesAlgebra.mem_grade_iff: the elements of degree n are the monomials r Xⁿ with r ∈ Iⁿ.
• reesAlgebra.isInternal_grade: the Rees algebra is the internal direct sum of its graded pieces.
• reesAlgebra.coe_decompose_apply: the degree n component of f is the monomial f.coeff n • Xⁿ.
• reesAlgebra.irrelevant_eq_span_monomialDegreeOne: if I is generated by a family s, the irrelevant ideal of R[It] is generated by the elements sᵢ t.

References

• The Stacks Project, Section Blowing up

noncomputable def reesAlgebra.grade {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : Submodule R ↥(reesAlgebra I)

The degree n piece of the Rees algebra R[It]: the monomials r Xⁿ with r ∈ Iⁿ.

Equations

• reesAlgebra.grade I n = Submodule.comap (reesAlgebra I).val.toLinearMap (Submodule.map (Polynomial.monomial n) (I ^ n))

theorem reesAlgebra.mem_grade_iff {R : Type u_1} [CommRing R] {I : Ideal R} {n : ℕ} {f : ↥(reesAlgebra I)} : f ∈ grade I n ↔ ∃ r ∈ I ^ n, (Polynomial.monomial n) r = ↑f

The elements of degree n of the Rees algebra are the monomials r Xⁿ with r ∈ Iⁿ.

theorem reesAlgebra.mem_grade_iff_monomial_coeff {R : Type u_1} [CommRing R] {I : Ideal R} {n : ℕ} {f : ↥(reesAlgebra I)} : f ∈ grade I n ↔ (Polynomial.monomial n) ((↑f).coeff n) = ↑f

An element of the Rees algebra has degree n exactly when it is the monomial of degree n formed by its n-th coefficient.

theorem reesAlgebra.monomial_mem_grade {R : Type u_1} [CommRing R] {I : Ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) : ⟨(Polynomial.monomial n) r, ⋯⟩ ∈ grade I n

The monomial r Xⁿ with r ∈ Iⁿ lies in degree n.

theorem reesAlgebra.coeff_eq_zero_of_mem_grade {R : Type u_1} [CommRing R] {I : Ideal R} {m n : ℕ} {f : ↥(reesAlgebra I)} (hf : f ∈ grade I n) (hmn : m ≠ n) : (↑f).coeff m = 0

The coefficients of an element of degree n vanish away from n.

instance reesAlgebra.gradedMonoid {R : Type u_1} [CommRing R] {I : Ideal R} : SetLike.GradedMonoid (grade I)

theorem reesAlgebra.isInternal_grade {R : Type u_1} [CommRing R] (I : Ideal R) : DirectSum.IsInternal (grade I)

The Rees algebra is the internal direct sum of its graded pieces.

@[instance_reducible]

noncomputable instance reesAlgebra.gradedAlgebra {R : Type u_1} [CommRing R] {I : Ideal R} : GradedAlgebra (grade I)

The grading of the Rees algebra R[It] by the power of t.

Equations

• reesAlgebra.gradedAlgebra = ⋯.gradedAlgebra

@[simp]

theorem reesAlgebra.coe_decompose_apply {R : Type u_1} [CommRing R] {I : Ideal R} (f : ↥(reesAlgebra I)) (n : ℕ) : ↑↑(((DirectSum.decompose (grade I)) f) n) = (Polynomial.monomial n) ((↑f).coeff n)

The degree n component of an element f of the Rees algebra is the monomial f.coeff n • Xⁿ.

noncomputable def reesAlgebra.gradeZeroEquiv {R : Type u_1} [CommRing R] (I : Ideal R) : R ≃+* ↥(grade I 0)

The degree zero piece of the Rees algebra is a copy of the base ring R.

Equations

• reesAlgebra.gradeZeroEquiv I = RingEquiv.ofBijective (algebraMap R ↥(reesAlgebra.grade I 0)) ⋯

theorem reesAlgebra.gradeZeroEquiv_apply {R : Type u_1} [CommRing R] (I : Ideal R) (r : R) : (gradeZeroEquiv I) r = (algebraMap R ↥(grade I 0)) r

@[simp]

theorem reesAlgebra.coe_gradeZeroEquiv {R : Type u_1} [CommRing R] (I : Ideal R) (r : R) : ↑↑((gradeZeroEquiv I) r) = Polynomial.C r

@[simp]

theorem reesAlgebra.gradeZeroEquiv_symm_apply {R : Type u_1} [CommRing R] (I : Ideal R) (f : ↥(grade I 0)) : (gradeZeroEquiv I).symm f = (↑↑f).coeff 0

noncomputable def reesAlgebra.monomialDegreeOne {R : Type u_1} [CommRing R] {I : Ideal R} {a : R} (ha : a ∈ I) : ↥(reesAlgebra I)

The element a t of degree one of the Rees algebra R[It], for a ∈ I.

Equations

• reesAlgebra.monomialDegreeOne ha = ⟨(Polynomial.monomial 1) a, ⋯⟩

@[simp]

theorem reesAlgebra.coe_monomialDegreeOne {R : Type u_1} [CommRing R] {I : Ideal R} {a : R} (ha : a ∈ I) : ↑(monomialDegreeOne ha) = (Polynomial.monomial 1) a

theorem reesAlgebra.monomialDegreeOne_mem_grade {R : Type u_1} [CommRing R] {I : Ideal R} {a : R} (ha : a ∈ I) : monomialDegreeOne ha ∈ grade I 1

theorem reesAlgebra.irrelevant_eq_span_monomialDegreeOne {R : Type u_1} [CommRing R] {I : Ideal R} {ι : Type u_2} {s : ι → R} (hs : Ideal.span (Set.range s) = I) : (HomogeneousIdeal.irrelevant (grade I)).toIdeal = Ideal.span (Set.range fun (i : ι) => monomialDegreeOne ⋯)

The irrelevant ideal of the Rees algebra. If the ideal I is generated by a family s, then the irrelevant ideal ⨁_{n > 0} Iⁿ tⁿ of R[It] is generated by the elements sᵢ t of degree one.