The blowup of the node xy = πⁿ⁺² at its origin

Let π be a nonzerodivisor of a commutative ring R, for instance a uniformizer of a discrete valuation ring, let A = R[x, y] ⧸ (xy - πⁿ⁺²) and let I = (π, x, y) be the ideal of the origin (TauCeti.NodeAlgebra.originIdeal). This file describes the blowup Proj A[It] of Spec A along V(I) as a scheme over Spec R:

• it is covered by three open charts, the π-chart Spec R[u, v] ⧸ (uv - πⁿ) and, for each coordinate, the chart Spec R[x, t] ⧸ (xt - π);
• consequently it is flat, locally of finite presentation and of pure relative dimension one over Spec R, like Spec A itself.

When R is a discrete valuation ring with uniformizer π, the coordinate charts are regular and the π-chart is regular exactly when n ≤ 1. So a single blowup of the origin turns the nodes xy = π² and xy = π³ into regular schemes, while for n ≥ 2 the blowup is still singular.

Over a discrete valuation ring, this says that blowing up the singular point of the local model xy = πⁿ⁺² of a node yields again a flat, finitely presented relative curve, whose only possibly singular chart is the node xy = πⁿ of thickness lowered by two, while the two other charts are nodes of thickness one, regular at their origin (TauCeti.isRegularLocalRing_localization_quotient_X_mul_X_sub_C_pow_iff_of_irreducible).

Main definitions

• TauCeti.NodeAlgebra.blowupToSpec π n: the structure morphism Proj A[It] ⟶ Spec R of the blowup.
• TauCeti.NodeAlgebra.blowupBaseChartι: the open immersion of the π-chart Spec R[u, v] ⧸ (uv - πⁿ) into the blowup.
• TauCeti.NodeAlgebra.blowupCoordChartι: the open immersion of the chart Spec R[x, t] ⧸ (xt - π) of a coordinate xᵢ into the blowup.

Main results

• TauCeti.NodeAlgebra.opensRange_blowupBaseChartι_sup_iSup_opensRange_blowupCoordChartι: the three charts cover the blowup.
• TauCeti.NodeAlgebra.blowupBaseChartι_blowupToSpec, TauCeti.NodeAlgebra.blowupCoordChartι_blowupToSpec: the charts are morphisms over Spec R.
• TauCeti.NodeAlgebra.flat_blowup, TauCeti.NodeAlgebra.locallyOfFinitePresentation_blowup, TauCeti.NodeAlgebra.pureRelativeDimension_blowup: the blowup is flat, locally of finite presentation and of pure relative dimension one over Spec R.
• TauCeti.NodeAlgebra.isRegularLocalRing_stalk_blowup_iff: over a discrete valuation ring, every local ring of the blowup is regular exactly when n ≤ 1.

References

• The Stacks Project, Example 55.14.1
• The Stacks Project, Section Blowing up

noncomputable def TauCeti.NodeAlgebra.blowupToSpec {R : Type u} [CommRing R] (π : R) (n : ℕ) : AlgebraicGeometry.Proj (reesAlgebra.grade (originIdeal π (π ^ (n + 2)))) ⟶ AlgebraicGeometry.Spec ↧R

The structure morphism Proj A[It] ⟶ Spec A ⟶ Spec R of the blowup of A = R[x, y] ⧸ (xy - πⁿ⁺²) along I = (π, x, y), as a scheme over Spec R.

Equations

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

theorem TauCeti.NodeAlgebra.blowupToSpec_def {R : Type u} [CommRing R] (π : R) (n : ℕ) : blowupToSpec π n = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (reesAlgebra.grade (originIdeal π (π ^ (n + 2))))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (reesAlgebra.gradeZeroEquiv (originIdeal π (π ^ (n + 2)))).toCommRingCatIso.hom) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R (π ^ (n + 2)))))))

noncomputable def TauCeti.NodeAlgebra.blowupBaseChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.Spec ↧(NodeAlgebra R (π ^ n)) ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade (originIdeal π (π ^ (n + 2))))

The π-chart of the blowup of a node. For a nonzerodivisor π of R, the open immersion Spec R[u, v] ⧸ (uv - πⁿ) ⟶ Proj A[It] into the blowup of A = R[x, y] ⧸ (xy - πⁿ⁺²) along I = (π, x, y), with u = x/π and v = y/π. Its image is the standard open D₊(π t).

Equations

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

instance TauCeti.NodeAlgebra.instIsOpenImmersionBlowupBaseChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.IsOpenImmersion (blowupBaseChartι n hπ)

theorem TauCeti.NodeAlgebra.opensRange_blowupBaseChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.Scheme.Hom.opensRange (blowupBaseChartι n hπ) = AlgebraicGeometry.Proj.basicOpen (reesAlgebra.grade (originIdeal π (π ^ (n + 2)))) (reesAlgebra.monomialDegreeOne ⋯)

The π-chart of the blowup of the node is an open immersion onto the standard open D₊(π t).

@[simp]

theorem TauCeti.NodeAlgebra.blowupBaseChartι_blowupToSpec {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : CategoryTheory.CategoryStruct.comp (blowupBaseChartι n hπ) (blowupToSpec π n) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R (π ^ n))))

The π-chart of the blowup of the node is a morphism over Spec R: followed by the structure map Proj A[It] ⟶ Spec A ⟶ Spec R, it is the structure map of R[u, v] ⧸ (uv - πⁿ).

@[simp]

theorem TauCeti.NodeAlgebra.blowupBaseChartι_blowupToSpec_assoc {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (blowupBaseChartι n hπ) (CategoryTheory.CategoryStruct.comp (blowupToSpec π n) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R (π ^ n))))) h

The π-chart of the blowup of the node is a morphism over Spec R: followed by the structure map Proj A[It] ⟶ Spec A ⟶ Spec R, it is the structure map of R[u, v] ⧸ (uv - πⁿ).

noncomputable def TauCeti.NodeAlgebra.blowupCoordChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (i : Fin 2) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.Spec ↧(NodeAlgebra R π) ⟶ AlgebraicGeometry.Proj (reesAlgebra.grade (originIdeal π (π ^ (n + 2))))

The coordinate charts of the blowup of a node. For a nonzerodivisor π of R, the open immersion Spec R[x, t] ⧸ (xt - π) ⟶ Proj A[It] into the blowup of A = R[x₀, x₁] ⧸ (x₀x₁ - πⁿ⁺²) along I = (π, x₀, x₁), with x = xᵢ and t = π/xᵢ. Its image is the standard open D₊(xᵢ t).

Equations

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

instance TauCeti.NodeAlgebra.instIsOpenImmersionBlowupCoordChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (i : Fin 2) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.IsOpenImmersion (blowupCoordChartι n i hπ)

theorem TauCeti.NodeAlgebra.opensRange_blowupCoordChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (i : Fin 2) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.Scheme.Hom.opensRange (blowupCoordChartι n i hπ) = AlgebraicGeometry.Proj.basicOpen (reesAlgebra.grade (originIdeal π (π ^ (n + 2)))) (reesAlgebra.monomialDegreeOne ⋯)

The chart of the coordinate xᵢ of the blowup of the node is an open immersion onto the standard open D₊(xᵢ t).

@[simp]

theorem TauCeti.NodeAlgebra.blowupCoordChartι_blowupToSpec {R : Type u} [CommRing R] {π : R} (n : ℕ) (i : Fin 2) (hπ : π ∈ nonZeroDivisors R) : CategoryTheory.CategoryStruct.comp (blowupCoordChartι n i hπ) (blowupToSpec π n) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R π)))

The chart of a coordinate of the blowup of the node is a morphism over Spec R: followed by the structure map Proj A[It] ⟶ Spec A ⟶ Spec R, it is the structure map of R[x, t] ⧸ (xt - π).

@[simp]

theorem TauCeti.NodeAlgebra.blowupCoordChartι_blowupToSpec_assoc {R : Type u} [CommRing R] {π : R} (n : ℕ) (i : Fin 2) (hπ : π ∈ nonZeroDivisors R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (blowupCoordChartι n i hπ) (CategoryTheory.CategoryStruct.comp (blowupToSpec π n) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R π)))) h

The chart of a coordinate of the blowup of the node is a morphism over Spec R: followed by the structure map Proj A[It] ⟶ Spec A ⟶ Spec R, it is the structure map of R[x, t] ⧸ (xt - π).

The open cover by the three charts

theorem TauCeti.NodeAlgebra.opensRange_blowupBaseChartι_sup_iSup_opensRange_blowupCoordChartι {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.Scheme.Hom.opensRange (blowupBaseChartι n hπ) ⊔ ⨆ (i : Fin 2), AlgebraicGeometry.Scheme.Hom.opensRange (blowupCoordChartι n i hπ) = ⊤

The charts cover the blowup of a node. For a nonzerodivisor π of R, the blowup of A = R[x₀, x₁] ⧸ (x₀x₁ - πⁿ⁺²) along I = (π, x₀, x₁) is covered by the π-chart Spec R[u, v] ⧸ (uv - πⁿ) and the charts Spec R[x, t] ⧸ (xt - π) of the two coordinates.

The blowup as a relative curve over Spec R

theorem TauCeti.NodeAlgebra.flat_blowup {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.Flat (blowupToSpec π n)

The blowup of a node is flat. For a nonzerodivisor π of R, the blowup of R[x, y] ⧸ (xy - πⁿ⁺²) along (π, x, y) is flat over Spec R.

theorem TauCeti.NodeAlgebra.locallyOfFinitePresentation_blowup {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.LocallyOfFinitePresentation (blowupToSpec π n)

The blowup of a node is locally of finite presentation. For a nonzerodivisor π of R, the blowup of R[x, y] ⧸ (xy - πⁿ⁺²) along (π, x, y) is locally of finite presentation over Spec R.

theorem TauCeti.NodeAlgebra.pureRelativeDimension_blowup {R : Type u} [CommRing R] {π : R} (n : ℕ) (hπ : π ∈ nonZeroDivisors R) : AlgebraicGeometry.PureRelativeDimension 1 (blowupToSpec π n)

The blowup of a node has pure relative dimension one. For a nonzerodivisor π of R, every fibre of the blowup of R[x, y] ⧸ (xy - πⁿ⁺²) along (π, x, y) over Spec R is a curve all of whose irreducible components are one-dimensional.

Regularity of the blowup over a discrete valuation ring

theorem TauCeti.NodeAlgebra.isRegularLocalRing_stalk_blowup_iff {R : Type u} [CommRing R] {π : R} (n : ℕ) [IsDomain R] [IsDiscreteValuationRing R] (hπ : Irreducible π) : (∀ (x : ↥(AlgebraicGeometry.Proj (reesAlgebra.grade (originIdeal π (π ^ (n + 2)))))), IsRegularLocalRing ↑((AlgebraicGeometry.Proj (reesAlgebra.grade (originIdeal π (π ^ (n + 2))))).presheaf.stalk x)) ↔ n ≤ 1

One blowup resolves a node of thickness two or three. For a uniformizer π of a discrete valuation ring R, every local ring of the blowup of R[x, y] ⧸ (xy - πⁿ⁺²) along (π, x, y) is regular exactly when n ≤ 1.