Theorem 97: the setting and the induction, in marked form #
[Kol07, Theorem 97] and its proof: with ψ, ψ' : U ⇉ X the maps of an étale equivalence and
B^U := ψ^*B = ψ'^*B' the common pull-back, the proof is an induction on the stage carrying
(1) (X_i, I_i) = (X'_i, I'_i), (2) the lifts ψ_i, ψ'_i : U_i ⇉ X_i satisfy
im(ψ^*_i − ψ'^*_i) ⊂ (Π^U_i)^{-1}_*(MC(I^U_0), 1), (3) Z_{i−1} = Z'_{i−1}, with the remark that
Z^U_i ⊂ W_i := cosupp((Π^U_i)^{-1}_*(MC(I^U_0), 1)) by Corollary 77. This file recasts the
induction in a marked form: the datum carried along the induction is the marked ideal
(M, 1), M := MC(ψ^*I), with M_i := (Π^U_i)^{-1}_*(M, 1) ≤ 𝒪(Z^U_i) (the containment of
ideals, IsMarkedOneSeq of Hironaka/Resolution/Algebraic/MaximalContact/Theorem97Setup.lean), and
no property of I is used; indeed the transforms I_i are, as the Warning in [Kol07, 104] says, in
general neither D-balanced nor MC-invariant.
- The setting:
C = ψ^*Bis a smooth blow-up sequence of ordermfor(U, ψ^*I, ψ^{-1}E)(IsOrderSeq.pullbackalong the étaleψ) and has no empty centre. - The marked ideals: [Kol07, Corollary 77] with
j = m − 1(IsOrderSeq.leOrdAlong_markedTransformSeq_MC) givesord_{Z^U_i} M_i ≥ 1; the centres are smooth, hence reduced, soM_i ≤ 𝒪(Z^U_i), the hypothesis (ii) of the marked form. The containment must be one of ideals: for a non-reduced centreJ = (x², y²)andM = (x, y)have equal zero sets butM ⊄ J. - The lifts: the stage lifts
ψ_iare étale (base change), and every centre ofB(ofB') lies in the image of the lift ofψ(ofψ'),CentersInRange, because the centres of an order-msequence lie overcosupp(I, m) ⊆ im ψ: the hypothesis (iii). - The induction: a structural induction on the common pull-back
C, generalizing the baseXand the sequences and maps. ForC = cons U Z^U C₁bothBandB'arecons, withZ.comap ψ = Z^U = Z'.comap ψ'; the first centres are equal by the descent of closed subschemes along flat maps agreeing on the common preimage (eq_of_comap_eq_of_agreeOn; Kollár'sZ_i = ψ_i(Z^U_i) = ψ'_i(Z^U_i) = Z'_i), and after the substitutionZ' := Zthe two liftsblowUpMap ψ Z,blowUpMap ψ' Z, the second transported to the common source alongZ.comap ψ = Z.comap ψ', agree onV(π^{-1}_*(M, 1))by the one-step descent of agreement through a blow-up, taken here as an explicit hypothesishstepin its exact statement and proved asagreeOn_blowUpMapinHironaka/Resolution/Algebraic/MaximalContact/AgreeOnBlowUpKernel.lean; the two are combined inHironaka/Resolution/Algebraic/MaximalContact/Theorem97.lean. The tails are handled by the induction hypothesis. - Theorem 97 from the marked form: with
M := MC(ψ^*I), (i) is condition (2) of [Kol07, Definition 96], (ii) the marked ideals, (iii) the lifts.
The étale part of Kollár's assertion (2), "ψ, ψ' lift to étale surjections
ψ_i, ψ'_i : U_i ⇉ X_i" (proof of [Kol07, Theorem 97]): the stage lifts of an étale ψ are
étale, by base change along the cartesian squares isPullback_pullbackStageHom.
Kollár's common pull-back B^U: the pull-back ψ^*B of a smooth blow-up sequence of order m
for (X, I, E) along the étale ψ of an étale equivalence is a smooth blow-up sequence of order
m for (U, ψ^*I, ψ^{-1}E) (IsOrderSeq.pullback along a map smooth of relative dimension
0).
The common pull-back of an étale equivalence has no empty centre when B has none: every centre
of the order-m sequence B lies over cosupp(I, m) ⊆ im ψ (centersInRange_of_cosupp_le_range,
noEmptyCenters_pullback_of_centersInRange).
Kollár's "étale surjections ψ_i" in the form where images contain the cosupport: every centre
of B lies in the image of the corresponding lift of ψ,
Z_i ⊆ Π_i^{-1}(cosupp(I, m)) ⊆ Π_i^{-1}(im ψ) = im ψ_i.
The second map: every centre of B' lies in the image of the corresponding lift of ψ'.
Kollár's "note that Z^U_i ⊂ W_i by (77)" (proof of [Kol07, Theorem 97]): for m ≥ 1 the
common pull-back C = ψ^*B is of order ≥ 1 for the marked ideal (MC(ψ^*I), 1) in the
containment form, M_i = (Π^U_i)^{-1}_*(MC(ψ^*I), 1) ≤ 𝒪(Z^U_i) at every stage:
[Kol07, Corollary 77] with j = m − 1 (IsOrderSeq.leOrdAlong_markedTransformSeq_MC) gives
ord_{Z^U_i} M_i ≥ 1, and the centre Z^U_i is smooth, hence reduced, so M_i ≤ 𝒪(Z^U_i)
(le_of_leOrdAlong_one_of_smooth on the stage U_i, smooth of relative dimension n over k).
The marked form of [Kol07, Theorem 97], given the one-step descent: for flat
ψ, ψ' : U ⟶ X, an ideal sheaf M on U, and blow-up sequences B, B' on X with a common
pull-back C = ψ^*B = ψ'^*B', if (i) ψ, ψ' agree on V(M), (ii) C is of order ≥ 1 for
(M, 1) (IsMarkedOneSeq), and (iii) the centres of B (of B') lie in the images of the lifts
of ψ (of ψ'), then B = B', given the one-step descent of agreement through a blow-up (the
hypothesis hstep, in the exact shape of agreeOn_blowUpMap). Structural induction on C: for
nil, both sequences have length 0 (length_pullback); for cons U Z^U C₁, both sequences are
cons with Z.comap ψ = Z^U = Z'.comap ψ' (the injectivity of cons, then the substitution
Z^U := Z.comap ψ), the first centres are equal by the descent of closed subschemes along flat
maps agreeing on the common preimage (eq_of_comap_eq_of_agreeOn, the agreement on V(Z^U) from
V(M) by AgreeOn.mono and (ii) at stage 0), the lifts blowUpMap ψ Z and blowUpMap ψ' Z
(the latter transported to the common source along Z.comap ψ = Z.comap ψ') agree on
V(π^{-1}_*(M, 1)) by hstep, and the induction hypothesis applies to the tails with (ii), (iii)
read off by isMarkedOneSeq_cons_iff, centersInRange_cons_iff and the transports
pullback_eqToHom_comp, centersInRange_eqToHom_comp. Of Kollár's three assertions, (3) is the
descent, (1) the substitution, (2) hstep.
[Kol07, Theorem 97] reduced to the marked form: for X smooth of relative dimension n over
k of characteristic zero, m ≥ 1, smooth blow-up sequences B, B' of order m for (X, I, E),
(X, I, E') that are étale equivalent through e, and the one-step descent hstep, B = B': the
marked form with M := MC(ψ^*I); (i) is condition (2) of [Kol07, Definition 96] (e.h2), (ii) is
isMarkedOneSeq_pullback, (iii) is centersInRange/centersInRange'; étale maps are flat.