Hauser's examples of blowing up a product ideal #

Two examples of [Hau14] in which the blow-up of a product ideal is read as an iterated blow-up, through blowUp.exists_mulIso (the blow-up of I · J is, canonically, the blow-up of I followed by the blow-up of the inverse image of J) for the blow-up AlgebraicGeometry.Scheme.IdealSheafData.blowUp.

[Hau14, Example 4.50] asks to interpret the blow-up of 𝔸² in the ideal (x, y²)(x, y) as a composite of blow-ups in regular centers. The blow-up of 𝔸²_k in (x, y²)(x, y) is the point blow-up (center (x, y)) followed by the blow-up of the inverse image of (x, y²), canonically over 𝔸²_k.
[Hau14, Example 4.66]: the zero set in 𝔸³ of the non-reduced ideal (x, yz)(x, y)(x, z), printed there as (x³, x²y, x²z, xyz, y²z), is the union of the y- and the z-axis, and Hauser describes its blow-up as the composite of the blow-up with center (x, yz) and a point blow-up of the resulting threefold W₁ at its singular point. The blow-up of 𝔸³_k in (x, yz)(x, y)(x, z) is the blow-up with center (x, yz) followed by the blow-up of the inverse image of (x, y)(x, z); Hauser's identification of that second blow-up with the point blow-up of the singular point of W₁ is taken up in HironakaExamples/BlowUpComposite.lean. A remark on the printed generators, not checked in Lean (the MvPolynomial ideal computation is too expensive for the elaborator): expanding the eight products of generators gives (x, yz)(x, y)(x, z) = (x³, x²y, x²z, xyz, y²z²), and Hauser's printed last generator y²z is not in the product (its degree-3 part is spanned by x³, x²y, x²z, xyz, all divisible by x); the zero set V(x, yz) is the same either way.

Ideals of k[x, y, z] are read as ideal sheaves on 𝔸ⁿ_k = Spec k[x₁, …, xₙ] through specIdealSheaf, which is multiplicative (specIdealSheaf_mul).

source

@[reducible, inline]