The graded Rees algebra

Mathlib's reesAlgebra I is the subalgebra R[It] ⊆ R[t] of the polynomials whose i-th coefficient lies in I ^ i; it carries no grading there. The grading of [Hau14, Definition 4.6] gives the variable t degree 1, so that the i-th piece reesAlgebra.grading I i is Iⁱ tⁱ: the polynomials all of whose coefficients of index j ≠ i vanish. Mathlib's polynomial variable X plays the role of Hauser's t. The pieces are independent and span, since a polynomial is the sum of its monomials and is determined by its coefficients (the degree-n component of p is (coeff n p) tⁿ, reesAlgebra.component), and degrees add under products; so the Rees algebra is a graded R-algebra, reesAlgebra.gradedAlgebra, by Mathlib's constructor DirectSum.IsInternal.gradedAlgebra.

The degree-zero piece is R itself, embedded by g ↦ g · t⁰ (reesAlgebra.gradingZeroEquiv). A ring map φ : R → S with φ(I) ⊆ J sends Rees(I) into Rees(J) degreewise, by applying φ to the coefficients (reesAlgebra.mapOfLe); these are the transition maps of the relative Proj of the Rees algebra of an ideal sheaf [TSPA, Tags 01OF and 0804].

R is any commutative ring and I any ideal: finiteness of I belongs to the properness of the blow-up, not to the construction. For I = 0 the Rees algebra is R in degree 0 and 0 in positive degrees; for I = R it is R[t] with the degree grading; for the zero ring everything is 0 [Hau14, Definition 4.6].

def reesAlgebra.grading {R : Type u} [CommRing R] (I : Ideal R) (i : ℕ) : Submodule R ↥(reesAlgebra I)

The graded pieces of the Rees algebra [Hau14, Definition 4.6]: the variable t has degree 1, so that the elements of Iⁱ · tⁱ have degree i. The i-th piece is the R-submodule of reesAlgebra I of the polynomials all of whose coefficients of index j ≠ i vanish, that is, of the monomials c tⁱ with c ∈ I ^ i (reesAlgebra.eq_monomial_of_mem_grading).

Equations

• reesAlgebra.grading I i = { carrier := {p : ↥(reesAlgebra I) | ∀ (j : ℕ), j ≠ i → (↑p).coeff j = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem reesAlgebra.mem_grading_iff {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {p : ↥(reesAlgebra I)} : p ∈ grading I n ↔ ∀ (j : ℕ), j ≠ n → (↑p).coeff j = 0

Membership: p has degree n iff its coefficients of index ≠ n vanish.

theorem reesAlgebra.coeff_eq_zero_of_mem_grading {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {p : ↥(reesAlgebra I)} (hp : p ∈ grading I n) {j : ℕ} (hj : j ≠ n) : (↑p).coeff j = 0

theorem reesAlgebra.coeff_mem_pow {R : Type u} [CommRing R] {I : Ideal R} (p : ↥(reesAlgebra I)) (n : ℕ) : (↑p).coeff n ∈ I ^ n

The n-th coefficient of an element of the Rees algebra lies in I ^ n (mem_reesAlgebra_iff, read on the subtype).

theorem reesAlgebra.eq_monomial_of_mem_grading {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {p : ↥(reesAlgebra I)} (hp : p ∈ grading I n) : ↑p = (Polynomial.monomial n) ((↑p).coeff n) ∧ (↑p).coeff n ∈ I ^ n

The normal form: an element of degree n is the monomial c tⁿ of its n-th coefficient c, and c ∈ I ^ n.

theorem reesAlgebra.mem_grading_of_coe_eq_monomial {R : Type u} [CommRing R] {I : Ideal R} {i : ℕ} {p : ↥(reesAlgebra I)} {c : R} (hp : ↑p = (Polynomial.monomial i) c) : p ∈ grading I i

An element of the Rees algebra that is a monomial of degree i lies in the i-th piece.

theorem reesAlgebra.mem_grading_iff_exists {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {p : ↥(reesAlgebra I)} : p ∈ grading I n ↔ ∃ c ∈ I ^ n, ↑p = (Polynomial.monomial n) c

The n-th piece consists of the monomials c tⁿ, c ∈ I ^ n.

noncomputable def reesAlgebra.component {R : Type u} [CommRing R] (I : Ideal R) (n : ℕ) : ↥(reesAlgebra I) →ₗ[R] ↥(grading I n)

The degree-n component (coeff n p) tⁿ of an element p of the Rees algebra, as an element of the n-th piece; R-linear in p. It recovers a homogeneous element of degree n (reesAlgebra.component_of_mem) and kills one of any other degree (reesAlgebra.component_of_mem_of_ne).

Equations

• reesAlgebra.component I n = { toFun := fun (p : ↥(reesAlgebra I)) => ⟨⟨(Polynomial.monomial n) ((↑p).coeff n), ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem reesAlgebra.component_of_mem {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {p : ↥(reesAlgebra I)} (hp : p ∈ grading I n) : (component I n) p = ⟨p, hp⟩

theorem reesAlgebra.component_of_mem_of_ne {R : Type u} [CommRing R] {I : Ideal R} {m n : ℕ} {p : ↥(reesAlgebra I)} (hp : p ∈ grading I m) (h : m ≠ n) : (component I n) p = 0

theorem reesAlgebra.component_coeAddMonoidHom {R : Type u} [CommRing R] {I : Ideal R} (x : DirectSum ℕ fun (i : ℕ) => ↥(grading I i)) (n : ℕ) : (component I n) ((DirectSum.coeAddMonoidHom (grading I)) x) = x n

Independence: the n-th component of a finite sum of homogeneous elements is its degree-n summand — a polynomial is determined by its coefficients, and the n-th coefficient of the sum is the n-th coefficient of the degree-n summand.

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

1 = 1 · t⁰ has degree 0, and the product c tⁱ · d tʲ = cd tⁱ⁺ʲ of elements of degrees i and j has degree i + j (Polynomial.monomial_mul_monomial).

theorem reesAlgebra.isInternal_grading {R : Type u} [CommRing R] (I : Ideal R) : DirectSum.IsInternal (grading I)

reesAlgebra I is the internal direct sum of its pieces [Hau14, Definition 4.6]. Independence is reesAlgebra.component_coeAddMonoidHom (compare coefficients); spanning is Polynomial.as_sum_support, each monomial monomial i (coeff i p) lying in the i-th piece by reesAlgebra.monomial_mem.

@[instance_reducible]

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

The grading on the Rees algebra, reesAlgebra I = ⨁ᵢ Iⁱ tⁱ as a graded R-algebra [Hau14, Definition 4.6], from Mathlib's constructor DirectSum.IsInternal.gradedAlgebra applied to reesAlgebra.isInternal_grading.

Equations

• reesAlgebra.gradedAlgebra I = ⋯.gradedAlgebra

theorem reesAlgebra.mem_grading_zero_iff {R : Type u} [CommRing R] {I : Ideal R} {p : ↥(reesAlgebra I)} : p ∈ grading I 0 ↔ ∃ (r : R), ↑p = Polynomial.C r

Degree zero consists of the constant polynomials [Hau14, Definition 4.6].

theorem reesAlgebra.algebraMap_mem_grading_zero {R : Type u} [CommRing R] {I : Ideal R} (r : R) : (algebraMap R ↥(reesAlgebra I)) r ∈ grading I 0

The constant r · t⁰ has degree zero.

noncomputable def reesAlgebra.gradingZeroEquiv {R : Type u} [CommRing R] (I : Ideal R) : ↥(grading I 0) ≃+* R

Degree zero is R [Hau14, Definition 4.6]: R embeds into the Rees algebra by sending g to the degree-zero element g · t⁰. An element of degree zero is the constant polynomial of its constant coefficient, and r ∈ R goes to the constant algebraMap R (reesAlgebra I) r. The compatibility with the grading-induced algebra structure is reesAlgebra.algebraMap_gradingZeroEquiv_symm.

Equations

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

noncomputable def reesAlgebra.mapOfLe {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S) {I : Ideal R} {J : Ideal S} (hIJ : Ideal.map φ I ≤ J) : grading I →+*ᵍ grading J

The graded ring map Rees(I) → Rees(J) induced by φ : R →+* S when φ(I) ⊆ J: ∑ pₙ tⁿ ↦ ∑ φ(pₙ) tⁿ [TSPA, Tag 01OF].

Equations

• reesAlgebra.mapOfLe φ hIJ = { toRingHom := (Polynomial.mapRingHom φ).restrict (reesAlgebra I) (reesAlgebra J) ⋯, map_mem := ⋯ }