The universal property of the affine blow-up in Hauser's Example 4.34

Let B = B_{(x,y)} 𝔸²_k = affineBlowUp (x, y) over k[x, y] = MvPolynomial (Fin 2) k be the blow-up of the plane at the origin, [Hau14, Example 4.34] (see also [TSPA, Tag 0806]).

• (i) The two k-points (1 : 0) and (0 : 1) of the exceptional ℙ¹ over the origin (the points x = 0, y/x = 0 of the chart Spec k[x, y/x] and y = 0, x/y = 0 of the chart Spec k[x/y, y]) are distinct morphisms Spec k ⟶ B with the same composite to 𝔸²_k (the origin). So uniqueness of lifts fails without admissibility: Spec k → 𝔸² at the origin pulls (x, y) back to 0, which is not invertible. Distinctness: a common value would lie in both charts, hence in D(y/x) ⊆ Spec k[x, y/x], but the point (1 : 0) has y/x = 0.
• (ii) The chart map chart x ≫ π : Spec k[x, y/x] ⟶ 𝔸²_k is admissible (its inverse image of (x, y) is the exceptional ideal on the chart, (x) with x a nonzerodivisor) and the chart immersion is its unique lift.

The k-points are built from the isomorphism k[x, y][(x, y)/x] ≅ k[x, y] (coordinateSubspaceEquiv), x ↦ x, y/x ↦ y, composed with evaluation at the origin.

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.center (k : Type u) [Field k] : Ideal (MvPolynomial (Fin 2) k)

The center (x, y) ⊆ k[x, y], as the coordinate ideal of the subset {0, 1}.

Equations

• Hironaka.BlowUp.Examples.center k = AlgebraicGeometry.affineBlowUpAlgebra.coordinateIdeal k {0, 1}

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.x₀ (k : Type u) [Field k] : ↥(center k)

x ∈ (x, y).

Equations

• Hironaka.BlowUp.Examples.x₀ k = ⟨MvPolynomial.X 0, ⋯⟩

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.x₁ (k : Type u) [Field k] : ↥(center k)

y ∈ (x, y).

Equations

• Hironaka.BlowUp.Examples.x₁ k = ⟨MvPolynomial.X 1, ⋯⟩

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.evalOrigin (k : Type u) [Field k] : MvPolynomial (Fin 2) k →ₐ[k] k

Evaluation at the origin.

Equations

• Hironaka.BlowUp.Examples.evalOrigin k = MvPolynomial.aeval fun (x : Fin 2) => 0

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.e₀ (k : Type u) [Field k] : ↥(AlgebraicGeometry.affineBlowUpAlgebra (AlgebraicGeometry.affineBlowUpAlgebra.coordinateIdeal k {0, 1}) (MvPolynomial.X 0)) ≃ₐ[k] MvPolynomial (Fin 2) k

The chart isomorphism k[x, y][(x, y)/x] ≅ k[x, y], x ↦ x, y/x ↦ y.

Equations

• Hironaka.BlowUp.Examples.e₀ k = AlgebraicGeometry.affineBlowUpAlgebra.coordinateSubspaceEquiv k {0, 1} 0

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.e₁ (k : Type u) [Field k] : ↥(AlgebraicGeometry.affineBlowUpAlgebra (AlgebraicGeometry.affineBlowUpAlgebra.coordinateIdeal k {0, 1}) (MvPolynomial.X 1)) ≃ₐ[k] MvPolynomial (Fin 2) k

The chart isomorphism k[x, y][(x, y)/y] ≅ k[x, y], y ↦ y, x/y ↦ x.

Equations

• Hironaka.BlowUp.Examples.e₁ k = AlgebraicGeometry.affineBlowUpAlgebra.coordinateSubspaceEquiv k {0, 1} 1

noncomputable def Hironaka.BlowUp.Examples.pt₀ (k : Type u) [Field k] : ↥(AlgebraicGeometry.affineBlowUpAlgebra (center k) (MvPolynomial.X 0)) →+* k

The k-point (1 : 0): x = 0, y/x = 0 in the chart k[x, y/x] ≅ k[x, y].

Equations

• Hironaka.BlowUp.Examples.pt₀ k = (↑(Hironaka.BlowUp.Examples.evalOrigin k)).comp ↑(Hironaka.BlowUp.Examples.e₀ k)

noncomputable def Hironaka.BlowUp.Examples.pt₁ (k : Type u) [Field k] : ↥(AlgebraicGeometry.affineBlowUpAlgebra (center k) (MvPolynomial.X 1)) →+* k

The k-point (0 : 1): y = 0, x/y = 0 in the chart k[x/y, y] ≅ k[x, y].

Equations

• Hironaka.BlowUp.Examples.pt₁ k = (↑(Hironaka.BlowUp.Examples.evalOrigin k)).comp ↑(Hironaka.BlowUp.Examples.e₁ k)

theorem Hironaka.BlowUp.Examples.pt₀_apply (k : Type u) [Field k] (z : ↥(AlgebraicGeometry.affineBlowUpAlgebra (center k) (MvPolynomial.X 0))) : (pt₀ k) z = (evalOrigin k) ((e₀ k) z)

theorem Hironaka.BlowUp.Examples.pt₁_apply (k : Type u) [Field k] (z : ↥(AlgebraicGeometry.affineBlowUpAlgebra (center k) (MvPolynomial.X 1))) : (pt₁ k) z = (evalOrigin k) ((e₁ k) z)

theorem Hironaka.BlowUp.Examples.pt₀_comp_algebraMap (k : Type u) [Field k] : (pt₀ k).comp (algebraMap (MvPolynomial (Fin 2) k) ↥(AlgebraicGeometry.affineBlowUpAlgebra (center k) (MvPolynomial.X 0))) = ↑(evalOrigin k)

Both k-points restrict to evaluation at the origin on k[x, y].

theorem Hironaka.BlowUp.Examples.pt₁_comp_algebraMap (k : Type u) [Field k] : (pt₁ k).comp (algebraMap (MvPolynomial (Fin 2) k) ↥(AlgebraicGeometry.affineBlowUpAlgebra (center k) (MvPolynomial.X 1))) = ↑(evalOrigin k)

theorem Hironaka.BlowUp.Examples.pt₀_ratio (k : Type u) [Field k] : (pt₀ k) (AlgebraicGeometry.affineBlowUpAlgebra.ratio (center k) (x₀ k) (x₁ k)) = 0

The point (1 : 0) has y/x = 0.

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.g₀ (k : Type u) [Field k] : AlgebraicGeometry.Spec ↧k ⟶ AlgebraicGeometry.affineBlowUp (center k)

The two k-points as morphisms Spec k ⟶ B.

Equations

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

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.g₁ (k : Type u) [Field k] : AlgebraicGeometry.Spec ↧k ⟶ AlgebraicGeometry.affineBlowUp (center k)

Equations

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

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.Examples.origin (k : Type u) [Field k] : ↥(AlgebraicGeometry.Spec ↧k)

The closed point of Spec k.

Equations

• Hironaka.BlowUp.Examples.origin k = { asIdeal := ⊥, isPrime := ⋯ }