The graded Rees algebra is generated in degree one

The Rees algebra of I is generated by its elements of degree one [Hau14, Definition 4.6], and Proj of the Rees algebra is covered by the D₊(a t), a ∈ I, because these elements generate the irrelevant ideal [TSPA, Tag 0804]. Mathlib has the subalgebra statement adjoin_monomial_eq_reesAlgebra; what Proj.affineOpenCoverOfIrrelevantLESpan needs is the ideal statement proved here: the irrelevant ideal HomogeneousIdeal.irrelevant (grading I) (the elements with vanishing degree-zero component) lies in Ideal.span (Set.range (reesAlgebra.degreeOne I)).

The argument

An element x of the Rees algebra is the sum of its homogeneous components (DirectSum.sum_support_decompose); if x is in the irrelevant ideal the degree-zero component is 0, so it suffices to place every homogeneous element of positive degree in the ideal generated by degree one. Such an element is c tⁿ with c ∈ I ^ n and n = m + 1 (reesAlgebra.eq_monomial_of_mem_grading); writing c as a sum of products d · a with d ∈ I ^ m, a ∈ I (Submodule.mul_induction_on' on I ^ (m + 1) = I ^ m * I) gives c t^(m+1) = ∑ (d tᵐ) · (a t), a combination of the generators a t with coefficients in the Rees algebra (reesAlgebra.mem_span_degreeOne_of_coe_eq_monomial). This is the induction of Mathlib's monomial_mem_adjoin_monomial, run one step.

Boundary cases

For I = 0 the irrelevant ideal is 0 and the statement is trivial; for I = R the degree-one elements are the r t, and the irrelevant ideal is (t).

theorem reesAlgebra.mem_span_degreeOne_of_coe_eq_monomial {R : Type u} [CommRing R] (I : Ideal R) {n : ℕ} (hn : 0 < n) {c : R} (hc : c ∈ I ^ n) {p : ↥(reesAlgebra I)} (hp : ↑p = (Polynomial.monomial n) c) : p ∈ Ideal.span (Set.range ⇑(degreeOne I))

A monomial c tⁿ of positive degree n with c ∈ I ^ n lies in the ideal of the Rees algebra generated by the degree-one elements a t, a ∈ I [Hau14, Definition 4.6].

theorem reesAlgebra.irrelevant_le_span_degreeOne {R : Type u} [CommRing R] (I : Ideal R) : (HomogeneousIdeal.irrelevant (grading I)).toIdeal ≤ Ideal.span (Set.range ⇑(degreeOne I))

Generated in degree one [Hau14, Definition 4.6]; [TSPA, Tag 0804]: the irrelevant ideal of the graded Rees algebra lies in the ideal generated by the degree-one elements a t, a ∈ I. This is the hypothesis of Mathlib's Proj.affineOpenCoverOfIrrelevantLESpan, which covers the affine blow-up by the charts D₊(a t) (affineBlowUp.affineOpenCover).

theorem reesAlgebra.irrelevant_le_span_degreeOne_of_span_eq {R : Type u} [CommRing R] (I : Ideal R) (s : Set R) (hs : Ideal.span s = I) : (HomogeneousIdeal.irrelevant (grading I)).toIdeal ≤ Ideal.span (Set.range fun (x : ↑s) => (degreeOne I) ⟨↑x, ⋯⟩)

Generation in degree one from any generating set of I (for generators g₁, …, g_k of I the blow-up is covered by the charts of the gᵢ [Hau14, Theorem 4.19]): the irrelevant ideal lies in the ideal generated by the x t, x ∈ s, whenever s generates I — every a t, a ∈ I, is an R-combination of them, since a ↦ a t is R-linear. This covers the affine blow-up by the charts of a generating set (affineBlowUp.affineOpenCoverOfSpan; the empty set for I = 0).