The Rees algebra of an ideal sheaf

Let I ⊆ 𝒪_X be an ideal sheaf on a scheme X. Its Rees algebra is the graded 𝒪_X-algebra

𝒪_X ⊕ I ⊕ I² ⊕ ⋯ = ⨁ₙ Iⁿ,

whose degree-n component is the ideal sheaf Iⁿ and whose multiplication Iⁱ ⊗ Iʲ ⟶ Iⁱ⁺ʲ multiplies local functions. It is the graded subalgebra of the polynomial algebra 𝒪_X[t] with Iⁿ tⁿ in degree n. Every ideal sheaf is quasi-coherent (Scheme.IdealSheafData.isQuasicoherent_sheaf), so the Rees algebra is a graded quasi-coherent algebra, and its relative Proj over X is the blowup of X along the closed subscheme V(I). Over an affine open U its sections in degree n are the ideal I(U)ⁿ (Scheme.IdealSheafData.range_sheafι_app_pow).

The homogeneous multiplication is Scheme.IdealSheafData.sheafMul for the ideal sheaves Iⁱ and Iʲ, read through Iⁱ * Iʲ = Iⁱ⁺ʲ, and the unit is the identification 𝒪_X = I⁰. Each Iⁿ includes into 𝒪_X by a monomorphism, under which the multiplication becomes the multiplication 𝒪_X ⊗ 𝒪_X ≅ 𝒪_X of the structure sheaf (Scheme.IdealSheafData.reesMul_sheafι). The graded unit, associativity and commutativity laws are therefore those of the commutative monoid 𝒪_X in the symmetric monoidal category of 𝒪_X-modules.

Over an affine open U, the graded ring of sections ⨁ n, Γ(Iⁿ, U) of the Rees algebra is the Rees algebra Γ(X, U)[I(U)t] ⊆ Γ(X, U)[t] of the ideal I(U) ⊆ Γ(X, U) (Scheme.IdealSheafData.reesAlgebraSectionsEquiv): reading sections of Iⁿ as regular functions, a section x of Iⁿ corresponds to the monomial x tⁿ. This identifies the affine charts of the relative Proj of the Rees algebra with the blowups of affine schemes.

Main definitions

• Scheme.IdealSheafData.reesComponent I n: the homogeneous component Iⁿ.
• Scheme.IdealSheafData.reesMul I i j: the multiplication Iⁱ ⊗ Iʲ ⟶ Iⁱ⁺ʲ.
• Scheme.IdealSheafData.reesOne I: the unit 𝒪_X ⟶ I⁰.
• Scheme.IdealSheafData.reesAlgebra I: the Rees algebra ⨁ₙ Iⁿ, as a graded quasi-coherent 𝒪_X-algebra.
• Scheme.IdealSheafData.reesAlgebraSectionsEquiv I hU: over an affine open U, the isomorphism of Γ(X, U)-algebras from ⨁ n, Γ(Iⁿ, U) to the Rees algebra Γ(X, U)[I(U)t].

Main results

• Scheme.IdealSheafData.reesMul_sheafι and Scheme.IdealSheafData.reesOne_sheafι: the multiplication and the unit are the restrictions of those of 𝒪_X.
• Scheme.IdealSheafData.reesAlgebra_obj_X, Scheme.IdealSheafData.mul_reesAlgebra and Scheme.IdealSheafData.one_reesAlgebra: the homogeneous components, multiplication and unit of the Rees algebra.
• Scheme.IdealSheafData.coe_reesAlgebraSectionsEquiv_of and Scheme.IdealSheafData.reesAlgebraSectionsEquiv_mem_grade_iff: the isomorphism reesAlgebraSectionsEquiv sends a section x of Iⁿ to x tⁿ, and matches the gradings.

Implementation notes

The Rees algebra is built from the named family Scheme.IdealSheafData.reesComponent I, not from fun n ↦ (I ^ n).sheaf. GradedQuasicoherentAlgebra.ofHomogeneous states its unit, associativity and commutativity laws through the family applied to degrees, and the kernel instantiates them without beta-reducing, so with a fun it must match each law against beta-redexes. Where the monoidal structure of X.Modules can be unfolded, as when a non-module file or the API documentation asks for the equation lemma of reesAlgebra, the kernel unfolds that structure instead and does not finish. With the named family, each law is literally the hypothesis it discharges.

References

• The Stacks Project, Tag 01OF: the blowing up of a quasi-coherent sheaf of ideals is the relative Proj of ⨁ₙ Iⁿ.
• R. Hartshorne, Algebraic Geometry, Section II.7, Blowing up.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.IdealSheafData.reesComponent {X : Scheme} (I : X.IdealSheafData) (n : ℕ) : X.Modules

The homogeneous component Iⁿ of the Rees algebra of I: the ideal sheaf Iⁿ, as an 𝒪_X-module.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.reesMul {X : Scheme} (I : X.IdealSheafData) (i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (I.reesComponent i) (I.reesComponent j) ⟶ I.reesComponent (i + j)

The multiplication Iⁱ ⊗ Iʲ ⟶ Iⁱ⁺ʲ of the Rees algebra of I: multiplication of local functions, through Iⁱ * Iʲ = Iⁱ⁺ʲ.

theorem AlgebraicGeometry.Scheme.IdealSheafData.reesMul_sheafι {X : Scheme} (I : X.IdealSheafData) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (I.reesMul i j) (I ^ (i + j)).sheafι = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (I ^ i).sheafι (I ^ j).sheafι) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)).hom

The multiplication of the Rees algebra, followed by the inclusion Iⁱ⁺ʲ ⟶ 𝒪_X, is the inclusion Iⁱ ⊗ Iʲ ⟶ 𝒪_X ⊗ 𝒪_X followed by the multiplication of 𝒪_X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.reesMul_sheafι_assoc {X : Scheme} (I : X.IdealSheafData) (i j : ℕ) {Z : X.Modules} (h : SheafOfModules.unit X.ringCatSheaf ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (I.reesMul i j) (I ^ (i + j)).sheafι) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (I ^ i).sheafι (I ^ j).sheafι) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)).hom) h

The multiplication of the Rees algebra, followed by the inclusion Iⁱ⁺ʲ ⟶ 𝒪_X, is the inclusion Iⁱ ⊗ Iʲ ⟶ 𝒪_X ⊗ 𝒪_X followed by the multiplication of 𝒪_X.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.reesOne {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ I.reesComponent 0

The unit 𝒪_X ⟶ I⁰ of the Rees algebra of I: every regular function is a section of I⁰ = 𝒪_X.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.reesOne_sheafι {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.CategoryStruct.comp I.reesOne (I ^ 0).sheafι = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

The unit of the Rees algebra, followed by the inclusion I⁰ ⟶ 𝒪_X, is the identity.

theorem AlgebraicGeometry.Scheme.IdealSheafData.reesOne_sheafι_assoc {X : Scheme} (I : X.IdealSheafData) {Z : X.Modules} (h : SheafOfModules.unit X.ringCatSheaf ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp I.reesOne (I ^ 0).sheafι) h = h

The unit of the Rees algebra, followed by the inclusion I⁰ ⟶ 𝒪_X, is the identity.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.reesAlgebra {X : Scheme} (I : X.IdealSheafData) : TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra X

The Rees algebra ⨁ₙ Iⁿ of an ideal sheaf I, as a graded quasi-coherent 𝒪_X-algebra. Its degree-n component is the ideal sheaf Iⁿ (reesAlgebra_obj_X), its multiplication is multiplication of local functions (mul_reesAlgebra, reesMul_sheafι) and its unit is the identification 𝒪_X = I⁰ (one_reesAlgebra, reesOne_sheafι).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.reesAlgebra_obj_X {X : Scheme} (I : X.IdealSheafData) : I.reesAlgebra.obj.X = fun (n : ℕ) => (I ^ n).sheaf

The homogeneous components of the Rees algebra of I are the powers Iⁿ.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_reesAlgebra {X : Scheme} (I : X.IdealSheafData) (i j : ℕ) : I.reesAlgebra.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (I.reesMul i j) (CategoryTheory.eqToHom ⋯))

The homogeneous multiplication of the Rees algebra of I is reesMul, up to the identification reesAlgebra_obj_X of its components with the powers of I.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.one_reesAlgebra {X : Scheme} (I : X.IdealSheafData) : I.reesAlgebra.obj.toMon.one = CategoryTheory.CategoryStruct.comp I.reesOne (CategoryTheory.eqToHom ⋯)

The unit of the Rees algebra of I is reesOne, up to the identification reesAlgebra_obj_X of its degree-zero component with I⁰.

instance AlgebraicGeometry.Scheme.IdealSheafData.isIso_reesOne {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.IsIso I.reesOne

The unit 𝒪_X ⟶ I⁰ of the Rees algebra is an isomorphism, inverse to the inclusion I⁰ ⟶ 𝒪_X of the unit ideal sheaf.

instance AlgebraicGeometry.Scheme.IdealSheafData.isIso_one_reesAlgebra {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.IsIso I.reesAlgebra.obj.toMon.one

The unit 𝒪_X ⟶ I⁰ of the Rees algebra, as a commutative monoid object, is an isomorphism.

The sections of the Rees algebra

The Rees algebra of the sections over an affine open

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.reesAlgebraSectionsEquiv {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) : (DirectSum ℕ fun (n : ℕ) => ↑((I.reesAlgebra.obj.X n).presheaf.obj (Opposite.op U))) ≃ₐ[↑(X.presheaf.obj (Opposite.op U))] ↥(_root_.reesAlgebra (I.ideal ⟨U, hU⟩))

The sections of the Rees algebra over an affine open. Over an affine open U of X, the graded ring of sections ⨁ n, Γ(Iⁿ, U) of the Rees algebra of I is the Rees algebra Γ(X, U)[I(U)t] of the ideal I(U): a section x of Iⁿ corresponds to the monomial x tⁿ (coe_reesAlgebraSectionsEquiv_of), and this isomorphism matches the gradings (reesAlgebraSectionsEquiv_mem_grade_iff).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_reesAlgebraSectionsEquiv_of {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) (n : ℕ) (x : ↑((I.reesAlgebra.obj.X n).presheaf.obj (Opposite.op U))) : ↑((I.reesAlgebraSectionsEquiv hU) ((DirectSum.of (fun (n : ℕ) => ↑((I.reesAlgebra.obj.X n).presheaf.obj (Opposite.op U))) n) x)) = (Polynomial.monomial n) ((CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (I ^ n).sheafι U)) ((CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (CategoryTheory.eqToHom ⋯) U)) x))

The isomorphism reesAlgebraSectionsEquiv sends a section x of Iⁿ over U to the monomial x tⁿ, where x is read as a regular function through the inclusion Iⁿ ⟶ 𝒪_X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.reesAlgebraSectionsEquiv_mem_grade_iff {X : Scheme} (I : X.IdealSheafData) {U : X.Opens} (hU : IsAffineOpen U) {n : ℕ} {x : DirectSum ℕ fun (n : ℕ) => ↑((I.reesAlgebra.obj.X n).presheaf.obj (Opposite.op U))} : (I.reesAlgebraSectionsEquiv hU) x ∈ reesAlgebra.grade (I.ideal ⟨U, hU⟩) n ↔ x ∈ I.reesAlgebra.obj.gradedSectionsGrading U n

The isomorphism reesAlgebraSectionsEquiv matches the grading of ⨁ n, Γ(Iⁿ, U) by its summands with the grading of the Rees algebra Γ(X, U)[I(U)t] by the power of t.