Hauser's Exercise 4 on the order: the four coordinate hyperplanes of 𝔸⁴

Exercise 4 of Appendix B of [Hau03] asks for the strata of constant order of the union X of the four coordinate hyperplanes of 𝔸⁴, and of the subscheme Y = V(xᵏyˡzᵐwⁿ). Over a field K of characteristic zero and at the K-rational point a, the order of the ideal (xyzw) is the number of coordinates of a that vanish (ord_hauserEx4_eq_card), and the order of (xᵏyˡzᵐwⁿ) is the sum of the exponents of the coordinates that vanish at a (ord_hauserEx4_monomial_eq_sum); so the stratum of order j of X is the set of points with exactly j vanishing coordinates. Both follow from the computation of the order of a monomial at a rational point in Hironaka/Scheme/IdealSheaf/Order/AffineSpace.lean: the order is additive on the regular local ring at a, and ord_a xᵢ is 1 or 0 according as aᵢ vanishes. There the order at a rational point is read off the partial derivatives, as in Hau03, Appendix A, Exercise 1, through the derivative ideals of [Kol07, Definition 73]. Exercise 3 of the same appendix, f = x³ + yᵏzᵐ, is treated in HironakaExamples/OrderStrata.lean.

theorem Hironaka.Order.Examples.ord_hauserEx4_eq_card {K : Type u} [Field K] [CharZero K] (a : Fin 4 → K) : (AlgebraicGeometry.specIdealSheaf (Ideal.span {MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 * MvPolynomial.X 3})).ord (AlgebraicGeometry.ratPoint a) = ↑(Nat.card { i : Fin 4 // a i = 0 })

Hauser's Exercise 4, first part: the order of xyzw at the rational point a of 𝔸⁴ is the number of coordinates of a that vanish.

theorem Hironaka.Order.Examples.ord_hauserEx4_monomial_eq_sum {K : Type u} [Field K] [CharZero K] (e : Fin 4 → ℕ) (a : Fin 4 → K) : (AlgebraicGeometry.specIdealSheaf (Ideal.span {∏ i : Fin 4, MvPolynomial.X i ^ e i})).ord (AlgebraicGeometry.ratPoint a) = ∑ i : Fin 4, if a i = 0 then ↑(e i) else 0

Hauser's Exercise 4, second part: the order of xᵏyˡzᵐwⁿ at the rational point a is the sum of the exponents of the coordinates that vanish at a.