The graded Rees algebra of (x, y) ⊆ k[x, y], and the affine blow-up as Proj

[Hau14, Example 4.34]: for I = (x, y) ⊆ k[x, y] the graded Rees algebra is k[x, y, u, v]/(xv − yu) with deg x = deg y = 0, deg u = deg v = 1, where u = x t and v = y t. The examples of the first section check this against reesAlgebra: the degree-one piece is the k[x, y]-module generated by u and v; degree zero is k[x, y] (the ring isomorphism reesAlgebra.gradingZeroEquiv, and membership as the constant polynomials); and the relation x v = y u holds.

The second section checks that the graded Rees algebra of an arbitrary ideal I of a commutative ring R carries the instances Mathlib's Proj requires: the affine blow-up Proj (reesAlgebra.grading I), its structure map to Spec R through the degree-zero identification, the chart cover indexed by I through Proj.affineOpenCoverOfIrrelevantLESpan (the irrelevant ideal is generated by the degree-one elements a t, a ∈ I), and properness over Spec R for finitely generated I from reesAlgebra.finiteType_of_fg and Mathlib's instance IsProper (Proj.toSpecZero 𝒜). Each example elaborating is the check.

@[reducible, inline]

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

The ideal I = (x, y) of k[x, y] of Hauser's Example 4.34.

Equations

• Hironaka.BlowUp.Examples.xy k = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1}

noncomputable def Hironaka.BlowUp.Examples.u (k : Type u_1) [Field k] : ↥(reesAlgebra (xy k))

u = x t, a degree-one generator.

Equations

• Hironaka.BlowUp.Examples.u k = (reesAlgebra.degreeOne (Hironaka.BlowUp.Examples.xy k)) ⟨MvPolynomial.X 0, ⋯⟩

noncomputable def Hironaka.BlowUp.Examples.v (k : Type u_1) [Field k] : ↥(reesAlgebra (xy k))

v = y t, a degree-one generator.

Equations

• Hironaka.BlowUp.Examples.v k = (reesAlgebra.degreeOne (Hironaka.BlowUp.Examples.xy k)) ⟨MvPolynomial.X 1, ⋯⟩