The universal property of the blowup

Let I be an ideal of a commutative ring R and let π : Proj R[It] ⟶ Spec R be the blowup of Spec R along V(I). This file proves its universal property: a morphism f : T ⟶ Spec R along which the centre pulls back to an effective Cartier divisor, that is, for which the ideal sheaf I·𝒪_T is locally generated by a nonzerodivisor, factors through π, and the factorization is unique. No finiteness hypothesis on I and no hypothesis on T is needed.

Uniqueness. Locally on T, say on an affine open Spec B where I B = a B with a a nonzerodivisor, the open D(a) = Spec B_a is scheme-theoretically dense, because B → B_a is injective. Over D(a) the ideal I generates the unit ideal, so D(a) maps into the complement of the centre, over which π is an isomorphism (TauCeti.AlgebraicGeometry.isIso_morphismRestrict_toSpecZero_reesAlgebra_of_disjoint_zeroLocus). Two lifts therefore agree on D(a), and hence on Spec B, since Proj R[It] is separated over Spec R.

Existence. On such an affine open, the elements c ∈ B with c a = i for some i ∈ I generate the unit ideal (Ideal.span_setOf_mul_eq_eq_top). On the basic open D(c), the image of i is a nonzerodivisor generating I B_c, so the universal property of the affine blowup algebra R[I/i] (Ideal.affineBlowupLift) gives a morphism into the chart Spec R[I/i] ⟶ Proj R[It]. These local lifts agree on overlaps by uniqueness and glue.

The blowup along an ideal sheaf. The same universal property holds for the blowup Bl_I X ⟶ X of an arbitrary scheme X along an arbitrary ideal sheaf I (AlgebraicGeometry.Scheme.IdealSheafData.blowup): a morphism f : T ⟶ X along which the ideal sheaf I.comap f of the inverse image of V(I) is effective Cartier factors uniquely through Bl_I X. Over an affine open V of X, the blowup is the blowup of Spec Γ(X, V) along V(I(V)) (AlgebraicGeometry.Scheme.IdealSheafData.isPullback_blowupChart), and the inverse image of V(I) on V is cut out by I(V) (AlgebraicGeometry.Scheme.IdealSheafData.comap_fromSpec_eq_ofIdealTop). So on f⁻¹ V the affine universal property gives a lift through the chart over V, unique among all lifts into the blowup, and these lifts glue. Again no finiteness hypothesis on I is needed.

Together with the fact that the centre pulls back to an effective Cartier divisor on the blowup itself, this characterizes the blowup as the terminal morphism along which the centre becomes an effective Cartier divisor.

Main definitions

• TauCeti.AlgebraicGeometry.projReesAlgebraLift f hf: the morphism T ⟶ Proj R[It] lifting f : T ⟶ Spec R, when the centre pulls back to an effective Cartier divisor on T.
• AlgebraicGeometry.Scheme.IdealSheafData.blowupLift I f hf: the morphism T ⟶ Bl_I X lifting f : T ⟶ X, when I.comap f is an effective Cartier divisor on T.

Main results

• TauCeti.AlgebraicGeometry.projReesAlgebraLift_toSpecZero: the lift is a morphism over Spec R.
• TauCeti.AlgebraicGeometry.projReesAlgebra_hom_ext: two morphisms T ⟶ Proj R[It] over Spec R agree when the centre pulls back to an effective Cartier divisor on T.
• TauCeti.AlgebraicGeometry.existsUnique_comp_toSpecZero_reesAlgebra_eq_of_isEffectiveCartier: the universal property of the blowup of Spec R along V(I).
• AlgebraicGeometry.Scheme.IdealSheafData.blowupLift_blowupToBase, AlgebraicGeometry.Scheme.IdealSheafData.blowup_hom_ext and AlgebraicGeometry.Scheme.IdealSheafData.existsUnique_comp_blowupToBase_eq_of_isEffectiveCartier: the same statements for the blowup of a scheme along an ideal sheaf; AlgebraicGeometry.Scheme.IdealSheafData.comp_blowupLift is the naturality of the lift in T.

References

• The Stacks Project, Section Blowing up, the universal property of blowing up.
• The Stacks Project, Lemma 0806, the universal property of the blowing up of a scheme along a quasi-coherent sheaf of ideals.
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Proposition II.7.14.

theorem TauCeti.AlgebraicGeometry.projReesAlgebra_hom_ext {R : Type u} [CommRing R] {I : Ideal R} {T : AlgebraicGeometry.Scheme} {g₁ g₂ : T ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade I)} (h : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom))) (hf : ((AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)).comap (CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)))).IsEffectiveCartier) : g₁ = g₂

Uniqueness in the universal property of the blowup. Two morphisms T ⟶ Proj R[It] over Spec R are equal if the centre V(I) pulls back to an effective Cartier divisor on T.

noncomputable def TauCeti.AlgebraicGeometry.projReesAlgebraLift {R : Type u} [CommRing R] (I : Ideal R) {T : AlgebraicGeometry.Scheme} (f : T ⟶ AlgebraicGeometry.Spec ↧R) (hf : ((AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)).comap f).IsEffectiveCartier) : T ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade I)

The universal property of the blowup: the lift. If the centre V(I) pulls back to an effective Cartier divisor on T along f : T ⟶ Spec R, this is the morphism T ⟶ Proj R[It] over Spec R lifting f (projReesAlgebraLift_toSpecZero). It is the only such morphism (eq_projReesAlgebraLift). This is the scheme-level counterpart of the chart lift Ideal.affineBlowupLift.

theorem TauCeti.AlgebraicGeometry.projReesAlgebraLift_toSpecZero {R : Type u} [CommRing R] {I : Ideal R} {T : AlgebraicGeometry.Scheme} (f : T ⟶ AlgebraicGeometry.Spec ↧R) (hf : ((AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)).comap f).IsEffectiveCartier) : CategoryTheory.CategoryStruct.comp (projReesAlgebraLift I f hf) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)) = f

The lift projReesAlgebraLift I f hf is a morphism over Spec R.

theorem TauCeti.AlgebraicGeometry.projReesAlgebraLift_toSpecZero_assoc {R : Type u} [CommRing R] {I : Ideal R} {T : AlgebraicGeometry.Scheme} (f : T ⟶ AlgebraicGeometry.Spec ↧R) (hf : ((AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)).comap f).IsEffectiveCartier) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (projReesAlgebraLift I f hf) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom) h)) = CategoryTheory.CategoryStruct.comp f h

The lift projReesAlgebraLift I f hf is a morphism over Spec R.

theorem TauCeti.AlgebraicGeometry.eq_projReesAlgebraLift {R : Type u} [CommRing R] {I : Ideal R} {T : AlgebraicGeometry.Scheme} {f : T ⟶ AlgebraicGeometry.Spec ↧R} (hf : ((AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)).comap f).IsEffectiveCartier) {g : T ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade I)} (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)) = f) : g = projReesAlgebraLift I f hf

Every morphism T ⟶ Proj R[It] over Spec R lifting f is the lift projReesAlgebraLift.

theorem TauCeti.AlgebraicGeometry.existsUnique_comp_toSpecZero_reesAlgebra_eq_of_isEffectiveCartier {R : Type u} [CommRing R] {I : Ideal R} {T : AlgebraicGeometry.Scheme} {f : T ⟶ AlgebraicGeometry.Spec ↧R} (hf : ((AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)).comap f).IsEffectiveCartier) : ∃! g : T ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade I), CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade I)) (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv I).toCommRingCatIso.hom)) = f

The universal property of the blowup of an affine scheme. A morphism f : T ⟶ Spec R along which the centre V(I) pulls back to an effective Cartier divisor factors uniquely through the blowup Proj R[It] ⟶ Spec R.

The blowup of a scheme along an ideal sheaf

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowup_hom_ext {X T : Scheme} (I : X.IdealSheafData) {g₁ g₂ : T ⟶ I.blowup} (h : CategoryTheory.CategoryStruct.comp g₁ I.blowupToBase = CategoryTheory.CategoryStruct.comp g₂ I.blowupToBase) (hf : (I.comap (CategoryTheory.CategoryStruct.comp g₁ I.blowupToBase)).IsEffectiveCartier) : g₁ = g₂

Uniqueness in the universal property of the blowup along an ideal sheaf. Two morphisms T ⟶ Bl_I X over X are equal if the centre V(I) pulls back to an effective Cartier divisor on T.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.blowupLift {X T : Scheme} (I : X.IdealSheafData) (f : T ⟶ X) (hf : (I.comap f).IsEffectiveCartier) : T ⟶ I.blowup

The universal property of the blowup along an ideal sheaf: the lift. If the centre V(I) pulls back to an effective Cartier divisor on T along f : T ⟶ X, this is the morphism T ⟶ Bl_I X over X lifting f (blowupLift_blowupToBase). It is the only such morphism (eq_blowupLift).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupLift_blowupToBase {X T : Scheme} (I : X.IdealSheafData) (f : T ⟶ X) (hf : (I.comap f).IsEffectiveCartier) : CategoryTheory.CategoryStruct.comp (I.blowupLift f hf) I.blowupToBase = f

The lift I.blowupLift f hf is a morphism over X.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowupLift_blowupToBase_assoc {X T : Scheme} (I : X.IdealSheafData) (f : T ⟶ X) (hf : (I.comap f).IsEffectiveCartier) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.blowupLift f hf) (CategoryTheory.CategoryStruct.comp I.blowupToBase h) = CategoryTheory.CategoryStruct.comp f h

The lift I.blowupLift f hf is a morphism over X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_blowupLift {X T : Scheme} (I : X.IdealSheafData) {f : T ⟶ X} (hf : (I.comap f).IsEffectiveCartier) {g : T ⟶ I.blowup} (hg : CategoryTheory.CategoryStruct.comp g I.blowupToBase = f) : g = I.blowupLift f hf

Every morphism T ⟶ Bl_I X over X lifting f is the lift blowupLift.

theorem AlgebraicGeometry.Scheme.IdealSheafData.existsUnique_comp_blowupToBase_eq_of_isEffectiveCartier {X T : Scheme} (I : X.IdealSheafData) {f : T ⟶ X} (hf : (I.comap f).IsEffectiveCartier) : ∃! g : T ⟶ I.blowup, CategoryTheory.CategoryStruct.comp g I.blowupToBase = f

The universal property of the blowup along an ideal sheaf. A morphism f : T ⟶ X along which the centre V(I) pulls back to an effective Cartier divisor factors uniquely through the blowup Bl_I X ⟶ X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comp_blowupLift {X T : Scheme} (I : X.IdealSheafData) {T' : Scheme} (h : T' ⟶ T) (f : T ⟶ X) (hf : (I.comap f).IsEffectiveCartier) (hhf : (I.comap (CategoryTheory.CategoryStruct.comp h f)).IsEffectiveCartier) : CategoryTheory.CategoryStruct.comp h (I.blowupLift f hf) = I.blowupLift (CategoryTheory.CategoryStruct.comp h f) hhf

The lift to the blowup is natural in the source: precomposing the lift of f with h : T' ⟶ T gives the lift of h ≫ f.