Kollár's Example 14 on the instance m = 3, n = 2: the mechanism of maximal contact #
[Kol07, Example 14] is the motivating computation for hypersurfaces of maximal contact: for a
hypersurface f = yᵐ + b₂(x)y^{m−2} + ⋯ + b_m(x) = 0 of multiplicity m at the origin, blown up
at the origin in the chart x_i = x_i' x_n', y = y' x_n', the transform is
F = y'ᵐ + c₂ y'^{m−2} + ⋯ + c_m with c_i = π⁻¹_*(b_i, i) the marked transforms (Kollár's (14.2)
and (14.6)); ∂^{m−1}F/∂y'^{m−1} = m!·y' (14.3), so every point of multiplicity ≥ m lies on the
transform of H = (y = 0) (Claim 14.4); the other (m−1)-st partials restricted to y' = 0 are
(m − i)!·∂^{i−1} c_i (14.5); and a point of y' = 0 has multiplicity ≥ m iff mult c_i ≥ i
for all i (Claim 14.7). This file proves these statements on the instance m = 3, n = 2,
b₂ = x₁² + x₂³, b₃ = x₁⁴ + x₁x₂² + x₂⁵, in ℚ[x₁, x₂, y], with (14.7) at every ℚ-point of
y' = 0.
Tools (from HironakaExamples/MaximalContact/Example82.lean): orders are 𝔪_p-adic memberships;
non-memberships come from a partial derivative that does not vanish at the point
(pderiv_mem_pow_of_mem_pow_succ, eval_eq_zero_of_mem_span); the (14.7) equivalence uses that
the restriction ρ : y' ↦ 0 maps 𝔪_p^k into itself and that ∂_{y'} lowers the 𝔪_p-adic
order by one.
Kollár's (14.1) on the instance: mult₀ f = 3, b₂ ∈ 𝔪₀², b₃ ∈ 𝔪₀³.
Kollár's (14.2) with (14.6): the chart transforms σ' f = x₂'³·F, σ' b₂ = x₂'²·c₂,
σ' b₃ = x₂'³·c₃.
Kollár's (14.3): ∂²F/∂y'² = 3!·y'.
Kollár's Claim 14.4 on the instance: a ℚ-point of multiplicity ≥ 3 of F lies on
y' = 0.
Kollár's (14.5): the mixed second partials of F restricted to y' = 0 are ∂c₂/∂x'_j and
∂²c₃/∂x'_j∂x'_k.
Kollár's Claim 14.7 on the instance, at every ℚ-point of y' = 0:
mult_p F ≥ 3 ↔ mult_p c₂ ≥ 2 ∧ mult_p c₃ ≥ 3.
At the origin of the chart, F, c₂, c₃ have multiplicity < 2.
At the point (0, 1, 0) of the chart, F(p) = c₃(p) = 1.