Blowing up the origin of the node xy = πⁿ

Let π be a nonzerodivisor of a commutative ring R, for instance a uniformizer of a discrete valuation ring, and let A = R[x, y] ⧸ (xy - πⁿ⁺²). When R is a discrete valuation ring with uniformizer π, the closed point (π, x, y) is the only point at which Spec A is not regular. This file computes the three affine charts of the blowup of Spec A along the ideal I = (π, x, y), namely the affine blowup algebras A[I/π], A[I/x] and A[I/y]:

• the π-chart A[I/π] = A[x/π, y/π] is again a node, R[u, v] ⧸ (uv - πⁿ), with u = x/π and v = y/π;
• the x-chart A[I/x] = A[π/x, y/x] is R[x, t] ⧸ (xt - π), with t = π/x, and symmetrically for the y-chart.

Thus blowing up the origin replaces the thickness n + 2 of the node by n on the only chart that can still be singular, while the two other charts are nodes of thickness one, which over a discrete valuation ring are regular at their origin (TauCeti.isRegularLocalRing_localization_quotient_X_mul_X_sub_C_pow_iff_of_irreducible). This is the local computation behind the resolution of the nodes of a model of a curve over a discrete valuation ring by repeated blowups of closed points.

Main definitions

• TauCeti.NodeAlgebra.originIdeal π a: the ideal (π, x, y) of R[x, y] ⧸ (xy - a).

Main results

• TauCeti.NodeAlgebra.affineBlowupBaseEquiv: the π-chart of the blowup of xy = πⁿ⁺² at the origin is xy = πⁿ.
• TauCeti.NodeAlgebra.affineBlowupCoordEquiv: each coordinate chart of the blowup of xy = πⁿ⁺² at the origin is xy = π.

Implementation notes

Each chart is described by an explicit R-algebra map φ from a node algebra into a localization S of A, whose image is the affine blowup algebra. Injectivity of φ is proved by exhibiting a map ψ from S to a localization of the source of φ at a nonzerodivisor, such that ψ ∘ φ is the localization map: for the π-chart, ψ is induced by x ↦ πu, y ↦ πv, and for the x-chart by x ↦ x, y ↦ πⁿ⁺¹t.

References

• The Stacks Project, Example 55.14.1
• The Stacks Project, Section Blow up algebras

The ideal of the origin

noncomputable def TauCeti.NodeAlgebra.originIdeal {R : Type u_1} [CommRing R] (π a : R) : Ideal (NodeAlgebra R a)

The ideal (π, x, y) of R[x, y] ⧸ (xy - a). It cuts out the origin of the fibre over V(π); for a = πⁿ⁺² with π a uniformizer of a discrete valuation ring, it is the ideal of the singular point of the node.

Equations

• TauCeti.NodeAlgebra.originIdeal π a = Ideal.span {(algebraMap R (TauCeti.NodeAlgebra R a)) π, TauCeti.NodeAlgebra.coord a 0, TauCeti.NodeAlgebra.coord a 1}

theorem TauCeti.NodeAlgebra.originIdeal_def {R : Type u_1} [CommRing R] (π a : R) : originIdeal π a = Ideal.span {(algebraMap R (NodeAlgebra R a)) π, coord a 0, coord a 1}

@[simp]

theorem TauCeti.NodeAlgebra.algebraMap_mem_originIdeal {R : Type u_1} [CommRing R] (π a : R) : (algebraMap R (NodeAlgebra R a)) π ∈ originIdeal π a

@[simp]

theorem TauCeti.NodeAlgebra.coord_mem_originIdeal {R : Type u_1} [CommRing R] (π a : R) (i : Fin 2) : coord a i ∈ originIdeal π a

Images of algebra maps out of a node

The π-chart

noncomputable def TauCeti.NodeAlgebra.affineBlowupBaseEquiv {R : Type u_1} [CommRing R] {π : R} (n : ℕ) (S : Type u_2) [CommRing S] [Algebra R S] [Algebra (NodeAlgebra R (π ^ (n + 2))) S] [IsScalarTower R (NodeAlgebra R (π ^ (n + 2))) S] [IsLocalization.Away ((algebraMap R (NodeAlgebra R (π ^ (n + 2)))) π) S] (hπ : π ∈ nonZeroDivisors R) : NodeAlgebra R (π ^ n) ≃ₐ[R] ↥((originIdeal π (π ^ (n + 2))).affineBlowup ((algebraMap R (NodeAlgebra R (π ^ (n + 2)))) π) S)

The π-chart of the blowup of a node. For a nonzerodivisor π of R, let A = R[x, y] ⧸ (xy - πⁿ⁺²) and I = (π, x, y). The affine blowup algebra A[I/π] is the node R[u, v] ⧸ (uv - πⁿ), with u = x/π and v = y/π.

Equations

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

@[simp]

theorem TauCeti.NodeAlgebra.coe_affineBlowupBaseEquiv_coord {R : Type u_1} [CommRing R] {π : R} {n : ℕ} {S : Type u_2} [CommRing S] [Algebra R S] [Algebra (NodeAlgebra R (π ^ (n + 2))) S] [IsScalarTower R (NodeAlgebra R (π ^ (n + 2))) S] [IsLocalization.Away ((algebraMap R (NodeAlgebra R (π ^ (n + 2)))) π) S] (hπ : π ∈ nonZeroDivisors R) (i : Fin 2) : ↑((affineBlowupBaseEquiv n S hπ) (coord (π ^ n) i)) = Localization.divBy (coord (π ^ (n + 2)) i) ((algebraMap R (NodeAlgebra R (π ^ (n + 2)))) π)

The isomorphism R[u, v] ⧸ (uv - πⁿ) ≃ A[I/π] sends u to x/π and v to y/π.

The coordinate charts

noncomputable def TauCeti.NodeAlgebra.affineBlowupCoordEquiv {R : Type u_1} [CommRing R] {π : R} (n : ℕ) (i : Fin 2) (S : Type u_2) [CommRing S] [Algebra R S] [Algebra (NodeAlgebra R (π ^ (n + 2))) S] [IsScalarTower R (NodeAlgebra R (π ^ (n + 2))) S] [IsLocalization.Away (coord (π ^ (n + 2)) i) S] (hπ : π ∈ nonZeroDivisors R) : NodeAlgebra R π ≃ₐ[R] ↥((originIdeal π (π ^ (n + 2))).affineBlowup (coord (π ^ (n + 2)) i) S)

The coordinate charts of the blowup of a node. For a nonzerodivisor π of R, let A = R[x₀, x₁] ⧸ (x₀x₁ - πⁿ⁺²) and I = (π, x₀, x₁). For either coordinate xᵢ, the affine blowup algebra A[I/xᵢ] is the node R[x, t] ⧸ (xt - π), with x = xᵢ and t = π/xᵢ; the other coordinate becomes x_{1-i}/xᵢ = πⁿt².

Equations

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

@[simp]

theorem TauCeti.NodeAlgebra.coe_affineBlowupCoordEquiv_coord_zero {R : Type u_1} [CommRing R] {π : R} {n : ℕ} {i : Fin 2} {S : Type u_2} [CommRing S] [Algebra R S] [Algebra (NodeAlgebra R (π ^ (n + 2))) S] [IsScalarTower R (NodeAlgebra R (π ^ (n + 2))) S] [IsLocalization.Away (coord (π ^ (n + 2)) i) S] (hπ : π ∈ nonZeroDivisors R) : ↑((affineBlowupCoordEquiv n i S hπ) (coord π 0)) = (algebraMap (NodeAlgebra R (π ^ (n + 2))) S) (coord (π ^ (n + 2)) i)

The isomorphism R[x, t] ⧸ (xt - π) ≃ A[I/xᵢ] sends x to xᵢ.

@[simp]

theorem TauCeti.NodeAlgebra.coe_affineBlowupCoordEquiv_coord_one {R : Type u_1} [CommRing R] {π : R} {n : ℕ} {i : Fin 2} {S : Type u_2} [CommRing S] [Algebra R S] [Algebra (NodeAlgebra R (π ^ (n + 2))) S] [IsScalarTower R (NodeAlgebra R (π ^ (n + 2))) S] [IsLocalization.Away (coord (π ^ (n + 2)) i) S] (hπ : π ∈ nonZeroDivisors R) : ↑((affineBlowupCoordEquiv n i S hπ) (coord π 1)) = Localization.divBy ((algebraMap R (NodeAlgebra R (π ^ (n + 2)))) π) (coord (π ^ (n + 2)) i)

The isomorphism R[x, t] ⧸ (xt - π) ≃ A[I/xᵢ] sends t to π/xᵢ.