Kollár's Examples 11, 12 and 106: coordinates and charts #
Kollár's three running examples of maximal contact and of the uniqueness theorem for hypersurfaces
of maximal contact, [Kol07, Theorem 97], are computed in
Hironaka/Resolution/Algebraic/MaximalContact/: Example11Charts.lean and Example11Stages.lean
treat [Kol07, Example 11] (I = (x² + y³ − z⁶), m = 2, the hypersurfaces H = (x) and H' = (x + y²)), Example12Charts.lean and Example12Stages.lean treat [Kol07, Example 12]
(I = (x³ + (y² − z⁶)² + z²¹), m = 3, H = (x) and H' = (x + 3y² − z⁶)), and
Example106Charts.lean and Example106Stages.lean treat [Kol07, Example 106]
(I = (x³ − y², x⁴ + xz² − w³), m = 2, H = (y) and H' = (y − x²)). This file imports them
and records, as local notation, the coordinates of the polynomial rings, the substitutions
σx, σy, σz, σw giving the charts of the blow-up of the origin, the restriction ρH to the
hypersurface H = (x = 0), and the maximal ideal 𝔪(a, b, c, d) of a rational point; it declares
no constant of its own.
The computations in those files follow one pattern: each chart identity σ g = vᵐ · g' is a
polynomial identity, checked after evaluating the substitution on the variables; each order bound
J ≤ 𝔪_p^m is an explicit membership in a power of the maximal ideal of the ℚ-point p; each
strict bound ¬ J ≤ 𝔪_p^{m+1} and each computation of a locus evaluates iterated partial
derivatives at p (an element of 𝔪_p^{k+1} has all its k-th partials in 𝔪_p, hence
vanishing at p) and solves the resulting rational equations by case analysis; the equalities of
derivative ideals D, D² are proved in both directions, ⊆ from the partial derivatives of
the generators and ⊇ by explicit ℚ-linear combinations of them.