Hauser's Example 4.66: a blow-up of 𝔸³ as the composite of two blow-ups

[Hau14, Example 4.66] describes the blow-up of 𝔸³ with center the non-reduced ideal (x, yz)(x, y)(x, z) as the composite of two blow-ups: the first with center (x, yz), the second "the point blow-up of W₁ with center this singular point", W₁ the threefold the first produces. This file reads the statement through the two-step theorem blowUp.exists_comp_iso for the blow-up AlgebraicGeometry.Scheme.IdealSheafData.blowUp: the composite of the blow-up of 𝔸³_k with center (x, yz) and the blow-up of the inverse image of (x, y)(x, z) is a single blow-up of 𝔸³_k, canonically over 𝔸³_k, whose center is supported on V(x, yz), the union of the y- and z-axes: the image of the second center lies in V((x, y)(x, z)) = V(x, y) ∪ V(x, z) ⊆ V(x, yz). Hauser's identification of the inverse image of (x, y)(x, z) with the ideal of the singular point of W₁, up to the exceptional factor, is a chart computation that this file does not check. The centers center1 = (x, yz), zAxis = (x, y), yAxis = (x, z) are those of HironakaExamples/BlowUpProduct.lean.

theorem Hironaka.BlowUp.Examples.center1_le_zAxis (k : Type u) [Field k] : center1 k ≤ zAxis k

(x, yz) ⊆ (x, y): the z-axis lies in V(x, yz).

theorem Hironaka.BlowUp.Examples.center1_le_yAxis (k : Type u) [Field k] : center1 k ≤ yAxis k

(x, yz) ⊆ (x, z): the y-axis lies in V(x, yz).

theorem Hironaka.BlowUp.Examples.support_axes_subset (k : Type u) [Field k] : ↑(AlgebraicGeometry.specIdealSheaf (zAxis k * yAxis k)).support ⊆ ↑(AlgebraicGeometry.specIdealSheaf (center1 k)).support

V((x, y)(x, z)) ⊆ V(x, yz) as sets: support is antitone and specIdealSheaf is multiplicative and order-reflecting.