Going down along a blow-up: Kollár's Examples 82 and 14 #
[Kol07, Example 82] (I = (xy − zⁿ), ord₀ I = 2, D(I) = (x, y, z^{n−1}), and its second part:
f = x³ + xy⁵ + z⁴ with the general hypersurface of maximal contact
x + u₁xy³ + u₂y⁴ + u₃z² = 0, uᵢ units, followed through two blow-ups) and [Kol07, Example 14]
(the points of multiplicity m on the blow-up of a hypersurface lie on the birational transform
of the hyperplane y = 0) are computed in HironakaExamples/MaximalContact/Example82.lean and
Example14.lean. This file records the coordinate and chart notation of those computations and
states the eight results on the second part of Example 82 over an arbitrary nontrivial
commutative ℚ-algebra R, with the algebra instances of R as explicit hypotheses of each
theorem (in Example82.lean they are section variables): the orders at the origin of f (three)
and of the maximal-contact element h (one); h ∈ D²(f); the two chart rows σ f = y³ · f',
σ f' = y³ · f'' with the corresponding rows for h; the order of f'' at the origin (two); the
elimination identity writing (1 + u₁y³)³ f'' as a remainder plus a multiple of the transformed
h''; the membership of the remainder in (y³, y²z⁴); and its order at the origin (three, and
exactly three when u₂ is a unit).
All are computations in polynomial rings. The identities (the chart rows of Example 82, the
elimination identity, Example 14's transform and its formulas (14.3) and (14.5)) are polynomial
identities after the substitution lemmas of aeval; memberships in powers of a point's maximal
ideal are exhibited by witnesses; non-memberships (the exact orders and multiplicities) come from
two tools, a partial derivative lowers the power of an ideal by one (the Leibniz rule) and
evaluation at the point kills its maximal ideal, applied to a (k−1)-fold partial derivative that
does not vanish at the point; the derivative ideals are computed from the partial derivatives of
the generators (derivative_span_pderiv), with D(xy − zⁿ) = (x, y, z^{n−1}) from
derivative_example52; h ∈ D²(f) divides ∂∂f by nonzero rationals over the ℚ-algebra R;
[Kol07, Claim 14.7] at every ℚ-point of y' = 0 uses that the restriction y' ↦ 0 maps 𝔪_p^k
into itself and that ∂_{y'} lowers the order by one.
Example 82, first part: I = (xy − zⁿ) #
Example 82, second part: f = x³ + xy⁵ + z⁴ #
h ∈ D²(f) = MC(f): the maximal-contact element lies in the second derivative ideal of f.
The first blow-up, chart x = x₁y₁, y = y₁, z = z₁y₁: f and h transform to
y³ · (x³ + xy³ + yz⁴) and y · (x + u₁xy³ + u₂y³ + u₃yz²), Kollár's second row.
The second blow-up in the same chart: Kollár's third row, y³ · (x³ + xy + y²z⁴) and
y · (x + u₁xy³ + u₂y² + u₃y²z²).
The elimination identity: (1 + u₁y³)³ · f'' is a remainder free of x plus a multiple of the
transformed maximal-contact element h'' = x + u₁xy³ + u₂y² + u₃y²z²; so f'' restricted to
h'' = 0 is the remainder, up to the unit (1 + u₁y³)³.
The remainder lies in the ideal (y³, y²z⁴).