Going down: restriction of an order-m sequence to a hypersurface of maximal contact #
[Kol07, 51.1] and the second half of [Kol07, Definition 78]: for a hypersurface of maximal contact
H every centre Z_i of a smooth blow-up sequence of order m starting with (X, I) lies in the
strict transform H_i, and therefore the restriction
Π|_{H_r} : (H_r, I_r|_{H_r}, m) → ⋯ → (H_0, I|_H, m) is a smooth blow-up sequence of order ≥ m
starting with (H, I|_H, m); restriction is injective. The proof of [Kol07, Corollary 85] adds
the divisor E.
- Centres in
H_i. Definition 78 quantifies over every openX' ⊆ X; read onX' = Xitself (the identity open immersion) it saysZ_i ⊆ H_ifor the given sequence (strictTransformSeq_le_center_of_isDynamicMaximalContact), which makes the restrictionS|_H, thepullbackalongH.subschemeι([Kol07, Definition 30.2]), a smooth blow-up sequence onH(isSmooth_pullback_of_isDynamicMaximalContact). - The order goes up under restriction. Pointwise this is
ord_le_ord_comap(ord_p I ≤ ord_p (I|_S), the remark opening [Kol07, §9]); along a closed subsetZof a smooth variety,ord_Z I ≥ mmeansord_x I ≥ mat every point ofZ(leOrdAlong_iff_forall_mem), and the points ofg⁻¹(Z)map intoZ, soord_{g⁻¹ Z}(g^* I) ≥ mfor every morphismg(leOrdAlong_comap). - Lemma 62 iterated. Kollár's
J_i := (Π_i^H)_*^{-1}(I|_H, m)is the marked recursion of the restricted sequence started atI|_H; by [Kol07, Lemma 62] in the form ofHironaka/Scheme/BlowUpSequence/PullbackInduced.lean(markedTransform_comap_blowUpMap_of_pow_dvd, iterated asIsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom) it is the restriction of the marked transform(I_i, m)toH_i, and for a sequence of ordermthe marked transforms are the weak transformsI_i:J_i = I_i|_{H_i}(weakTransformSeq_comap_pullbackStageHom). WhenI|_His nonzero on every component ofHandm ≥ 1, no centre of the restricted sequence is a component of its stage (not_component_subset_center_pullback), so the caseZ = Hin which Kollár's remark after Lemma 62 says the lemma fails does not arise. - Going down.
isOrderGeSeq_pullback_of_strictTransformSeq_le: the conditions (1′)–(4′) of [Kol07, Definition 66] forS|_Hwith the data(I|_H, m, E|_H). (2′) smooth centres: fromZ_i ⊆ H_i. (3′) at stageithe centreZ_i ⊆ H_ihas simple normal crossings withE_i + H_i(hasSncWith_totalTransformSeq_append), hence, viewed inH_i, withE_i|_{H_i}(AlgebraicGeometry.hasSncWith_comap_of_isClosedImmersion), which is(E|_H)_i(totalTransformSeq_comap_pullback). (4′)ord_{Z_i}(J_i) ≥ m:J_i = I_i|_{H_i}andord_{Z_i} I_i = mgoes up under restriction. The static corollary (isOrderGeSeq_pullback_of_isMaximalContact) takesZ_i ⊆ H_ifrom [Kol07, Theorem 80 (1)] (IsOrderSeq.strictTransformSeq_le_center_of_le_MC); the dynamic corollary (isOrderGeSeq_pullback_of_isDynamicMaximalContact, the sentence of Definition 78 withE = ∅) from the first item, the family∅ + Hbeing simple normal crossing becauseHis a smooth divisor (isSnc_append_empty_of_isSmoothDivisor). Injectivity (pullback_injective_of_isDynamicMaximalContact, [Kol07, 51.1]) isj_* j^* B = B(pushforward_pullback_of_strictTransformSeq_le) for sequences with centres in theH_i.
Going down is the "onto" half of the correspondence of [Kol07, Corollary 85]
(Hironaka/Resolution/Algebraic/MaximalContact/GoingUpDown.lean); the other half, going up, is
Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean.
Definition 78 read on X itself, and the injection of 51.1 #
[Kol07, Definition 78] on the open X' = X: every centre of a smooth blow-up sequence of order
m starting with (X, I) lies in the strict transform of a hypersurface of maximal contact
H.
The restriction B|_H ([Kol07, Definition 30.2]) of a smooth blow-up sequence of order m for
(X, I) to a hypersurface of maximal contact is a smooth blow-up sequence on H, the first
assertion of the second half of [Kol07, Definition 78].
The injection of [Kol07, 51.1]: two smooth blow-up sequences of order m for (X, I) with the
same restriction to a hypersurface of maximal contact are equal, since j_* j^* B = B when every
centre lies in the H_i.
The order along a closed subset goes up under pull-back #
The inequality ord_p I ≤ ord_p (I|_S) opening [Kol07, §9], along a closed subset: on a smooth
variety, ord_Z I ≥ m gives ord_{g⁻¹ Z}(g^* I) ≥ m for every g : Y ⟶ X, since the order along
Z is the order at every point of Z, and the order at a point goes up under pull-back
(ord_le_ord_comap).
Lemma 62 iterated, and the restricted sequence #
[Kol07, Lemma 62] iterated: along a smooth blow-up sequence of order m for (X, I, E), the
marked recursion of the restricted sequence started at I|_H is I_i|_{H_i} at every stage,
since the marked transforms of a sequence of order m are the weak transforms I_i.
Going down (the second half of [Kol07, Definition 78], with the divisor E as in the proof
of [Kol07, Corollary 85]): for a smooth hypersurface H with H + E simple normal crossing and a
smooth blow-up sequence of order m for (X, I, E) whose centres lie in the strict transforms
H_i, the restriction S|_H is a smooth blow-up sequence of order ≥ m starting with
(H, I|_H, m, E|_H): smooth centres, simple normal crossings with (E|_H)_i = E_i|_{H_i}, and
ord_{Z_i}(I_i|_{H_i}) ≥ ord_{Z_i} I_i = m.
Going down in the static form: for a smooth hypersurface H with 𝒪_X(−H) ⊆ MC(I), m ≥ 1,
and H + E simple normal crossing, the centres lie in the H_i by [Kol07, Theorem 80 (1)]
(IsOrderSeq.strictTransformSeq_le_center_of_le_MC) and
isOrderGeSeq_pullback_of_strictTransformSeq_le applies.
The second half of [Kol07, Definition 78] as printed: going down in the dynamic form with the
empty divisor family; the family ∅ + H is simple normal crossing because H is a smooth
divisor.
The case Z = H of Kollár's remark after [Kol07, Lemma 62] does not arise: when I|_H is
nonzero on every irreducible component of H and m ≥ 1, no centre of the restricted sequence
contains an irreducible component of its stage (IsOrderGeSeq.not_component_subset_center on the
restricted sequence).