Base change of the Rees algebra

Let I be an ideal of a commutative ring R and let S be an R-algebra, with extended ideal IS = I.map (algebraMap R S). Extending scalars from R to S compares the two Rees algebras:

S ⊗[R] R[It] ⟶ S[(IS)t], s ⊗ f ↦ s · f,

where the coefficients of f ∈ R[It] ⊆ R[X] are mapped to S. This comparison is a surjective homomorphism of graded S-algebras, for the grading n ↦ (R[It]ₙ).baseChange S of the source. In degree n it is the multiplication map S ⊗[R] Iⁿ ⟶ (IS)ⁿ; when S is flat over R the latter is injective, and the comparison is an isomorphism of graded algebras.

Geometrically, Proj of the Rees algebra is the blowup of Spec R along V(I), so the surjectivity makes the blowup of Spec S along V(IS) a closed subscheme of the base change of the blowup of Spec R, and the flat case identifies the two. The comparison is the composite of S ⊗[R] R[It] ⟶ S ⊗[R] R[X] with Mathlib's polyEquivTensor'.

Main definitions

• reesAlgebra.baseChangeHom I S: the comparison S ⊗[R] R[It] →ₐ[S] S[(IS)t].
• reesAlgebra.baseChangeGradedAlgHom I S: the same comparison as a graded algebra homomorphism.
• reesAlgebra.baseChangeEquiv I S: for flat S, the comparison as an algebra isomorphism.
• reesAlgebra.baseChangeGradedAlgHomSymm I S: for flat S, its inverse as a graded algebra homomorphism.

Main results

• reesAlgebra.coe_baseChangeHom_tmul: the comparison sends s ⊗ f to s · f.
• reesAlgebra.baseChangeHom_surjective: the comparison is surjective.
• reesAlgebra.baseChangeHom_injective: for flat S, the comparison is injective.
• reesAlgebra.baseChangeHom_mem_grade_iff: for flat S, the comparison preserves and reflects degrees.
• reesAlgebra.baseChangeHom_baseChangeEquiv_symm_apply, reesAlgebra.baseChangeEquiv_symm_baseChangeHom_apply: for flat S, the comparison and the inverse of reesAlgebra.baseChangeEquiv cancel.

References

• The Stacks Project, Section Blowing up, where blowing up is shown to commute with flat base change.

noncomputable def reesAlgebra.baseChangeHom {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] : TensorProduct R S ↥(reesAlgebra I) →ₐ[S] ↥(reesAlgebra (Ideal.map (algebraMap R S) I))

The comparison S ⊗[R] R[It] →ₐ[S] S[(IS)t] between the base change of the Rees algebra of I and the Rees algebra of the extended ideal IS: it sends s ⊗ f to s · f, with the coefficients of f mapped to S (reesAlgebra.coe_baseChangeHom_tmul).

@[simp]

theorem reesAlgebra.coe_baseChangeHom_tmul {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] (s : S) (f : ↥(reesAlgebra I)) : ↑((baseChangeHom I S) (s ⊗ₜ[R] f)) = s • Polynomial.map (algebraMap R S) ↑f

The comparison sends s ⊗ f to s · f, with the coefficients of f mapped to S.

theorem reesAlgebra.baseChangeHom_surjective {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] : Function.Surjective ⇑(baseChangeHom I S)

The comparison of Rees algebras is surjective: the Rees algebra of IS is generated over S by the monomials a t with a ∈ I.

theorem reesAlgebra.baseChangeHom_injective {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] : Function.Injective ⇑(baseChangeHom I S)

The comparison of Rees algebras is injective after flat base change: for flat S, the inclusion R[It] ⊆ R[X] stays injective after tensoring with S.

theorem reesAlgebra.baseChangeHom_mem_grade {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] {n : ℕ} {x : TensorProduct R S ↥(reesAlgebra I)} (hx : x ∈ Submodule.baseChange S (grade I n)) : (baseChangeHom I S) x ∈ grade (Ideal.map (algebraMap R S) I) n

The comparison sends the base change of the degree n piece of R[It] into the degree n piece of S[(IS)t].

noncomputable def reesAlgebra.baseChangeGradedAlgHom {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] : (fun (n : ℕ) => Submodule.baseChange S (grade I n)) →ₐᵍ[S] grade (Ideal.map (algebraMap R S) I)

The comparison S ⊗[R] R[It] ⟶ S[(IS)t] as a homomorphism of graded S-algebras, for the grading n ↦ (R[It]ₙ).baseChange S of the source.

@[simp]

theorem reesAlgebra.baseChangeGradedAlgHom_apply {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] (x : TensorProduct R S ↥(reesAlgebra I)) : (baseChangeGradedAlgHom I S) x = (baseChangeHom I S) x

The graded comparison has the comparison reesAlgebra.baseChangeHom as underlying map.

theorem reesAlgebra.baseChangeGradedAlgHom_surjective {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] : Function.Surjective ⇑(baseChangeGradedAlgHom I S)

The graded comparison of Rees algebras is surjective.

@[simp]

theorem reesAlgebra.baseChangeHom_mem_grade_iff {R : Type u_1} [CommRing R] {I : Ideal R} {S : Type u_2} [CommRing S] [Algebra R S] [Module.Flat R S] {n : ℕ} {x : TensorProduct R S ↥(reesAlgebra I)} : (baseChangeHom I S) x ∈ grade (Ideal.map (algebraMap R S) I) n ↔ x ∈ Submodule.baseChange S (grade I n)

For flat S, the comparison of Rees algebras preserves and reflects degrees.

noncomputable def reesAlgebra.baseChangeEquiv {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] : TensorProduct R S ↥(reesAlgebra I) ≃ₐ[S] ↥(reesAlgebra (Ideal.map (algebraMap R S) I))

Rees algebras commute with flat base change: for flat S, the comparison S ⊗[R] R[It] ≃ₐ[S] S[(IS)t] is an isomorphism.

@[simp]

theorem reesAlgebra.baseChangeEquiv_apply {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] (x : TensorProduct R S ↥(reesAlgebra I)) : (baseChangeEquiv I S) x = (baseChangeHom I S) x

The isomorphism reesAlgebra.baseChangeEquiv is the comparison reesAlgebra.baseChangeHom.

noncomputable def reesAlgebra.baseChangeGradedAlgHomSymm {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] : grade (Ideal.map (algebraMap R S) I) →ₐᵍ[S] fun (n : ℕ) => Submodule.baseChange S (grade I n)

For flat S, the inverse of the comparison S ⊗[R] R[It] ≃ₐ[S] S[(IS)t] as a homomorphism of graded S-algebras.

@[simp]

theorem reesAlgebra.baseChangeGradedAlgHomSymm_apply {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] (x : ↥(reesAlgebra (Ideal.map (algebraMap R S) I))) : (baseChangeGradedAlgHomSymm I S) x = (baseChangeEquiv I S).symm x

The inverse graded comparison is the inverse of reesAlgebra.baseChangeEquiv.

@[simp]

theorem reesAlgebra.baseChangeHom_baseChangeEquiv_symm_apply {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] (x : ↥(reesAlgebra (Ideal.map (algebraMap R S) I))) : (baseChangeHom I S) ((baseChangeEquiv I S).symm x) = x

For flat S, the comparison undoes the inverse of reesAlgebra.baseChangeEquiv.

@[simp]

theorem reesAlgebra.baseChangeEquiv_symm_baseChangeHom_apply {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] (x : TensorProduct R S ↥(reesAlgebra I)) : (baseChangeEquiv I S).symm ((baseChangeHom I S) x) = x

For flat S, the inverse of reesAlgebra.baseChangeEquiv undoes the comparison.

theorem reesAlgebra.baseChangeGradedAlgHom_rightInverse {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] : Function.RightInverse ⇑(baseChangeGradedAlgHomSymm I S) ⇑(baseChangeGradedAlgHom I S)

For flat S, the inverse graded comparison is a right inverse of the graded comparison.

theorem reesAlgebra.baseChangeGradedAlgHom_leftInverse {R : Type u_1} [CommRing R] (I : Ideal R) (S : Type u_2) [CommRing S] [Algebra R S] [Module.Flat R S] : Function.LeftInverse ⇑(baseChangeGradedAlgHomSymm I S) ⇑(baseChangeGradedAlgHom I S)

For flat S, the inverse graded comparison is a left inverse of the graded comparison.