Theorem 80 (1): a smooth static hypersurface of maximal contact is dynamic #
Kollár's proof of [Kol07, Theorem 80 (1)], for a smooth blow-up sequence Π of order m starting
with (X, I) and a smooth H with 𝒪_X(−H) ⊆ MC(I):
- Corollary 77 at
j = m − 1.Πis a sequence of order≥ mfor(X, I, m), in the direction that needs nomax-ord I = m, because the marked transforms with markmof an order-msequence are its weak transforms (IsOrderSeq.isOrderGeSeq); so [Kol07, Corollary 77] makes(X_i, J_i, 1)a sequence of order≥ 1starting with(X, MC(I), 1)(IsOrderSeq.isOrderGeSeq_MC), whenceord_{Z_i} J_i ≥ 1at every centre (IsOrderSeq.leOrdAlong_markedTransformSeq_MC). - The induction. Along any sequence of order
≥ 1for(X, J, 1), a smoothHwith𝒪(−H) ⊆ Jkeeps𝒪(−H_i) ⊆ J_iandH_ismooth (IsOrderGeSeq.strictTransformSeq_le_and_isSmoothDivisor, by induction on the sequence): at each stepord_{Z_i} J_i ≥ 1forcesord_{Z_i} H_i ≥ 1, i.e.Z_i ⊆ H_ias closed subschemes, because the smooth centre is reduced (le_of_leOrdAlong_one_of_smooth: vanishing on the support of a reduced closed subscheme is membership in its ideal, stalkwise through the prime stalks of the centre), so the transform of a hypersurface through the centre (Hironaka/Resolution/Algebraic/MaximalContact/Transform.lean) applies:𝒪(−H_{i+1}) = (π_i)⁻¹_*(𝒪(−H_i), 1) ⊆ (π_i)⁻¹_*(J_i, 1) = J_{i+1}by the monotonicity of the marked transform, andH_{i+1}is smooth. Specialized toJ = MC(I)this is Kollár's "𝒪_{X_i}(−H_i) ⊂ J_ifor everyi", withZ_i ⊆ H_ifor every centre (IsOrderSeq.strictTransformSeq_le_center_of_le_MC) and, through Corollary 77'sJ_i ⊆ D^{m−1}(I_i), the fact behind the Warning in [Kol07, 104] (keep the transforms of the old hypersurface of maximal contact after each blow-up): the transformH_iis again a static hypersurface of maximal contact for(I_i, m)(IsOrderSeq.isMaximalContact_strictTransformSeq). - Theorem 80 (1). Definition 78 asks the containment on every open
X⁰for every order-msequence of(X⁰, I|_{X⁰}); the static hypothesis and the smoothness ofHrestrict toX⁰(Hironaka/Resolution/Algebraic/MaximalContact/Restrict.lean), and step 2 applies there. The hypotheseshI : max-ord I = mandhHI : I|_H ≠ 0are part of Kollár's statement of Theorem 80 (1) and are kept so that the theorem reads as printed. The proof does not need them: the containmentZ_i ⊆ H_icomes from Corollary 77 atj = m − 1applied to a sequence of orderm, for whichm ≥ 1and𝒪_X(−H) ⊆ MC(I) = D^{m−1}(I)suffice, the markmbeing a parameter ofMC f I mrather thanmax-ord I; andI|_H ≠ 0enters Kollár's Definition 78 only through its second half, the restricted sequence as a sequence for the marked ideal(H, I|_H, m), which the library'sIsDynamicMaximalContactdoes not include and whichHironaka/Resolution/Algebraic/MaximalContact/GoingDown.leantreats separately, with the nonvanishing ofI|_Hon the components ofHas the hypothesis ofnot_component_subset_center_pullback.
The containment Z_i ⊆ H_i is also [Wlo05, Lemma 2.7.6]. The results here feed going down
(GoingDown.lean), the local existence (Existence.lean), the induction for Theorem 97
(Theorem97Induction.lean) and the order reduction in the maximal contact case
(Hironaka/Resolution/Algebraic/OrderReduction/Step21MaximalContact.lean).
The reduced centre: vanishing along Z is membership in the ideal of Z #
Kollár's "ord_{Z_i} H_i ≥ 1. Thus Z_i ⊂ H_i" in the proof of [Kol07, Theorem 80]: an ideal
sheaf of order ≥ 1 along a smooth centre Z, vanishing at the generic points of Z and hence
(upper semicontinuity) at every point of Z, is contained in the ideal sheaf of Z: J lies in
the vanishing ideal of |Z|, the radical of Z, and the stalks of a smooth Z at its points are
prime, so radical.
Corollary 77 at j = m − 1 #
A smooth blow-up sequence of order m for (X, I, E) is one of order ≥ m for
(X, I, m, E): its marked transforms with mark m are its weak transforms
(IsOrderSeq.markedTransformSeq_eq_weakTransformSeq), along which the order is exactly m. This
direction needs no max-ord I = m.
Kollár's "applying (77) for j = m − 1" ([Kol07, Corollary 77]): along a smooth blow-up
sequence of order m for (X, I, E) with m ≥ 1, the marked transforms of (MC(I), 1) form a
sequence of order ≥ 1 starting with (X, MC(I), 1, E).
Kollár's ord_{Z_i} J_i ≥ 1: the marked transform J_i of (MC(I), 1) has order ≥ 1 along
every centre.
The induction along a sequence of order ≥ 1 #
The induction of the proof of [Kol07, Theorem 80 (1)] in its natural generality (compare
[Wlo05, Lemma 2.7.4 (1)]): along a smooth blow-up sequence of order ≥ 1 for (X, J, 1, E), a
smooth hypersurface H with 𝒪(−H) ⊆ J has smooth strict transforms H_i with 𝒪(−H_i) ⊆ J_i
at every stage. At each step ord_{Z_i} J_i ≥ 1 gives ord_{Z_i} H_i ≥ 1, hence Z_i ⊆ H_i for
the reduced centre, and strictTransform_eq_markedTransform_one turns the strict transform of
H_i into the marked transform (π_i)⁻¹_*(𝒪(−H_i), 1) ⊆ (π_i)⁻¹_*(J_i, 1).
Kollár's "𝒪_{X_i}(−H_i) ⊂ J_i for every i" in the proof of [Kol07, Theorem 80 (1)].
Kollár's "H_0 is smooth", carried along the sequence: every strict transform H_i is a
smooth hypersurface of X_i.
Kollár's "Thus Z_i ⊂ H_i for every i" in the proof of [Kol07, Theorem 80 (1)]: every centre
lies in the strict transform of H, as closed subschemes (H_i ≤ Z_i as ideal sheaves). This is
also [Wlo05, Lemma 2.7.6].
The transform H_i is again a static hypersurface of maximal contact for (I_i, m):
𝒪(−H_i) ⊆ J_i ⊆ D^{m−1}(I_i) by [Kol07, Corollary 77]. This is what lets the Warning in
[Kol07, 104] keep the transforms of the old hypersurface of maximal contact after each blow-up.
Theorem 80 (1) #
[Kol07, Theorem 80 (1)]: for X smooth over k of characteristic zero, I with
m = max-ord I ≥ 1, and a smooth hypersurface H with 𝒪_X(−H) ⊆ MC(I) and I|_H ≠ 0, H is a
hypersurface of maximal contact in the dynamic sense of [Kol07, Definition 78]: on every open X⁰
the static hypothesis and the smoothness of H restrict, and
IsOrderSeq.strictTransformSeq_le_center_of_le_MC puts every centre of every order-m sequence
of (X⁰, I|_{X⁰}) inside the transform of H ∩ X⁰. The hypotheses hI : max-ord I = m and
hHI : I|_H ≠ 0 are part of Kollár's statement and are kept so that the theorem reads as printed;
the proof does not need them, because the containment of the centres needs only m ≥ 1 and
𝒪_X(−H) ⊆ MC(I), and I|_H ≠ 0 concerns the restricted sequence, which is treated in
Hironaka/Resolution/Algebraic/MaximalContact/GoingDown.lean (module docstring, step 3).