Blowing up a principal ideal: Hauser's Examples 4.28, 4.29 and 4.31

Examples of [Hau14] on the affine model affineBlowUp of the blow-up of Spec R. The examples check:

• R[gt] ≅ R[v] for a nonzerodivisor g, as graded R-algebras ([Hau14, Example 4.29]): the isomorphism reesAlgebra.polynomialEquiv exists, sends v to g t, and sends each monomial r vⁿ into the degree-n piece; over a polynomial ring k[x] with g = x.
• B_{(g)} Spec R = Spec R for a nonzerodivisor g: the blow-up map of the affine model is an isomorphism; over k[x] with g = x (the blow-up of the affine line at the origin, a Cartier divisor, is the identity, [Hau14, Example 4.28]).
• The zero-divisor case, [Hau14, Example 4.31], in corrected form. For any g the single chart ring R[(g)/g] is the image of R in R_g, with kernel the g-power torsion T_g, so B_{(g)} Spec R = Spec (R/T_g); for h g = 0 the blow-up lies in V(h), which is what remains of Hauser's description of it as the subscheme cut out by h. Concrete instance: R = k × k, g = (0, 1), h = (1, 0), where T_g = (h) and the blow-up is the second point V(h) = Spec k. This is why the definition of an invertible ideal asks for a nonzerodivisor generator: without it the blow-up along (g) is the proper closed subscheme Spec (R/T_g), not Spec R.

The example R = k[x, y, z]/(xy, xz), g = x, T_x = (y, z), where Hauser's V(h) fails, is discussed in HironakaExamples/BlowUp.lean.