Hauser's examples of blow-ups of affine schemes #

Worked examples of [Hau14] on the blow-up AlgebraicGeometry.Scheme.IdealSheafData.blowUp and on its affine model affineBlowUp (the component blowUp.ι ⊤ of the blow-up of an affine scheme).

(i) [Hau14, Example 4.34]: B_{(x, y)} 𝔸²_k has the two charts k[x, y/x] and k[x/y, y], glued along k[x, y/x][x/y]. The chart rings are polynomial rings in two variables over k (coordinateSubspaceEquiv), with y/x ↦ y on the first chart (coordinateSubspaceEquiv_frac); the chart of x meets the chart of y in the basic open of the ratio y/x (affineBlowUp.chart_preimage_chart), i.e. k[x, y/x][1/(y/x)]. The exceptional divisor ℙ¹_k is described through its k-points in (iv).
(ii) [Hau14, Example 4.29]: B_{(g)} X = X for a nonzerodivisor g. The blow-up map IdealSheafData.blowUpπ (specIdealSheaf (g)) is an isomorphism (isIso_π_of_isInvertible), the ideal sheaf of (g) on Spec R being invertible; on the affine model this is affineBlowUp.isIso_π_span_singleton (HironakaExamples/TrivialBlowUp.lean).
(iii) [Hau14, Examples 4.31 and 4.32], in corrected form: B_{(g)} Spec R = Spec (R / T_g) with T_g the g-power torsion, because the chart ring R[(g)/g] is the image of R in R_g with kernel T_g (surjective_algebraMap_span_singleton, ker_algebraMap_span_singleton in HironakaExamples/TrivialBlowUp.lean; Hauser's V(h) is the case h · g = 0, and the blow-up lies in V(h)). The example R = k[x, y, z]/(xy, xz), g = x, T_x = (y, z), where the blow-up is smaller than V(h), is not formalized: its content is the torsion computation in the quotient ring, which the general kernel description already settles (ker = ⋃ₖ Ann(gᵏ)), and the equality ⋃ₖ Ann(xᵏ) = (y, z) in that ring is a hand computation.
(iv) ([TSPA, Tag 0806]) The two k-points (1 : 0) and (0 : 1) of the exceptional ℙ¹_k of B_{(x, y)} 𝔸²_k are distinct morphisms Spec k ⟶ B with equal composite to 𝔸²_k (HironakaExamples/AffineBlowUpUniversal.lean: g₀ k ≠ g₁ k, equal composites with affineBlowUp.π), so the blow-up map is not a monomorphism over the center.