The modified functor commutes with closed embeddings of empty divisor in codimension one #
Włodarczyk proves that the modified resolution commutes with closed embeddings by running the
algorithm's own descent ([Wlo09, §7.1]): for τ : S ↪ M a closed hypersurface with 𝓘 ⊇ I_S and
the empty boundary, the coordinates defining S are tangent directions of the ideal, the algorithm
passes to the hypersurface V(u₁) and replaces the ideal with its restriction, so the run on M
is the run on S pushed forward. In codimension one no cover and no induction enter: S itself
is a global hypersurface of maximal contact of (M, 𝓘, ∅), so the value of the modified functor
is the value of the modified first step with the class's hypersurface replaced by S, and that
value is the push-forward of the value of the functor one dimension down. This is the argument of
BOanFamOfInput_commutesWithClosedEmbeddingsOfEmptyDivisorFam (ClosedEmbeddingFam.lean; Kollár's
[Kol07, Theorem 103 (3)], proved in [Kol07, Theorem 103, Step 2.4]), both being instances of
BO.hfStep2FamOn_eq_pushforwardRestrict_of_global, at the modified datum stepBData, plus two
facts about the modified run. The general codimension is the chaining
along a flag of hypersurfaces of [Kol07, 108] (Functor/ChainClosedEmbeddingChain.lean); its
corollary for a tower, BMOmodFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all in
Functor/ChainClosedEmbeddingZero.lean, takes the codimension-one commutation as a hypothesis,
which Hironaka/Resolution/Analytic/Wlo09/Concrete.lean supplies from this module.
IsClosedSubmanifold.ord_le_one_of_idealSheaf_le,AnalyticTriple.boClass_one_of_idealSheaf_le: an ideal sheaf containing the ideal of a smooth hypersurface has order≤ 1everywhere (offSit is the unit ideal, onSit contains a local equation of order1; the remark in the proof of [Kol07, 108]), so(M, 𝓘 ⊇ I_S, ∅)is in the classBO_{n,1}.descentStateAux_L_eq_nil_of_eq_zero,BMOmod.stepAFamOn_eq_nil,BMOmod.stepACFunctor_seqOn_eq_nil: the rounds on the nonmonomial part and the monomial phase are idle on(M, 𝓘, ∅)withord 𝓘 ≤ 1: with the empty boundary the nonmonomial part is𝓘itself, the round bound is≤ 1 < 2 = tand the descent has no link; the monomial phase has no active member.AnalyticFamilyFunctor.composeOn_eq_of_firstList_eq_nilis the generic fact: the composite along induced triples with the first functor idle is the second functor's value (shrinkAppend_nil,induced_nil, the commutation with the outer open's inclusion,compat).BMOmod.coreModOn_eq_pushforwardRestrict_of_isNonzeroEverywhere: the modified core at a memberS(the other members empty) whose trace ideal is nonzero everywhere: the stopped locus is empty (Zminus1_one_eq_empty_of_isNonzeroEverywhere: a stopped point would make the trace the zero ideal),H⁺ = S, and the core is the push-forward of the value ofRon(S, J, ∅)(indifference to the all-empty trace boundary). This is simpler than the family of [Kol07, Lemma 102]: there is no empty first blow-up.BMOmod.stepBFunctor_seqOn_eq_pushforwardRestrict_of_global: the modified first step on(M, 𝓘 ⊇ I_S, ∅)withSa global hypersurface: the functor's value is the local functor's (stepBFunctor_fam_eq), Step 2 at the mark1alongS(BO.hfStep2FamOn_eq_pushforwardRestrict_of_global), Step 2.2 at the single memberSof∅ + Sbeing the modified core.BMOmod.modFunctor_commutesWithClosedEmbeddings_one,BMOmod.BMOmodFamOfInput_of_hid_commutesWithClosedEmbeddings_one: the commutation in codimension one for the modified functor at dimensionn(through the functor one dimension downR) and for every level of the tower (leveln + 1through leveln; level0the empty list on both sides). Stated forBMOmodFamOfInput_of_hid, generic in the transform identityhid.
Sources: [Wlo09, §7.1]; [Kol07, 34.3] (commutation with closed embeddings), [Kol07, 108] (the
reduction to a hypersurface; every local equation of S lies in 𝓘, so the maximal order is
1), [Kol07, Theorem 103 (3)] and [Kol07, Theorem 103, Step 2.4], the proof of
[Kol07, Lemma 102]. The statements themselves are not in the sources.
The value of the data of the step depends on the triple and the member only (a substitution;
the analogue of BDanFamData.fam_seqOn_congr).
The per-open push-forward of the empty list is the empty list (pushforwardRestrict_eq,
pullback_nil, pushforward_nil).
An ideal sheaf containing the ideal of a smooth hypersurface has order ≤ 1 everywhere (the
remark in the proof of [Kol07, 108]: every local equation of S lies in 𝓘, so the maximal order
is 1): off S it is the unit ideal (stalkIdeal_idealSheaf_of_notMem), on S it contains a
local equation, of order 1.
The triple (M, 𝓘 ⊇ I_S, ∅) is in the class BO_{n,1} (ord_le_one_of_idealSheaf_le for the
order clause; no member).
The composite when the first functor is idle: if the value of F on the outer chain open is
the empty list, the composite's value on U is the value of G on U: shrinkAppend_nil,
induced_nil, the commutation of G with the inclusion of the outer open
(CommutesWithLocalIsos.seqOn_eq_of_image_eq), the composite restriction U ≤ W 1, the
compatibility compat of G, and the deletions of empty blow-ups (the end of the proof of
BOanFamOfInput_commutesWithClosedEmbeddingsOfEmptyDivisorFam in ClosedEmbeddingFam.lean, made
generic).
The descent with 0 links is the initial state: its list is empty (BState.initialOf_L; the
index is kept as a variable for the dependent rewrite).
The rounds are idle when the bound is below the first round: the descent has
D + 1 − t = 0 links, the chain state is the initial state and the value is the empty list
(BState.initialOf_L, pullback_nil, eraseEmpty_nil).
The rounds and the monomial phase are idle on (M, 𝓘, ∅) with ord 𝓘 ≤ 1 (the situation of
[Wlo09, §7.1], where the maximal order is 1 by the remark of [Kol07, 108]): with the empty
boundary the nonmonomial part is 𝓘 itself (monomialPart_eq_top_of_activeMembers_eq_empty,
monomialPart_mul_nonmonomialPart), so the round bound is ≤ 1 < 2 = t and the rounds give the
empty list (stepAFamOn_eq_nil); the monomial phase has no active member
(step2bPhase_of_not_nonempty); the composite is the second functor's value
(composeOn_eq_of_firstList_eq_nil), the empty list.
The modified core at a member with empty stopped locus is the push-forward of the value of
the functor one dimension down on the member (the proof of [Kol07, Lemma 102] in the modified
form; the recursion of [Wlo09, Theorem 7.4.1]): on the member S := Eʲ of a boundary all of whose
other members are empty, with the trace J := 𝓘|_S nonzero everywhere, the stopped locus
Z_{−1}(𝓘, 1)(S) is empty (Zminus1_one_eq_empty_of_isNonzeroEverywhere: a stopped point would
make J the zero ideal), so H⁺ = S (coreModOn_eq_of_eq) and the core is the value of R on the
restricted triple pushed forward. The value of R on (S, J, ∅ + all-empty trace) is its value on
(S, J, ∅) (hRi), and the push-forward of a list without empty centres, cleaned, is itself
(noEmptyCenters_pushforwardRestrict).
The modified first step commutes with a global hypersurface of codimension one (Kol07,
Theorem 103 (3) and [Kol07, Theorem 103, Step 2.4]; [Wlo09, §7.1]): on (M, 𝓘 ⊇ I_S, ∅) with S a
closed hypersurface and J := 𝓘|_S nonzero everywhere, the value of stepBFunctor R … on U is
the per-open push-forward of the value of R on (S, J, ∅) at U_S: the functor's value is the
local functor's (stepBFunctor_fam_eq: S is a global hypersurface of maximal contact), and
BO.hfStep2FamOn_eq_pushforwardRestrict_of_global applies at the datum stepBData, Step 2.2 at
the single member S of ∅ + S being the modified core (greatestIdx_eq,
HFamData.fam_seqOn_congr), which is the push-forward
(coreModOn_eq_pushforwardRestrict_of_isNonzeroEverywhere).
The modified functor at dimension n commutes with closed embeddings of empty divisor in
codimension one ([Wlo09, §7.1]; [Kol07, 108]; the predicate
CommutesWithClosedEmbeddingsOfEmptyDivisorFam at s := 1, through the functor one dimension down
R): for (M, 𝓘 ⊇ I_S, ∅) with S a closed hypersurface and J = 𝓘|_S, the value of
modFunctor R … on U is the push-forward of the value of R on U_S. The order of 𝓘 is at
most 1 by I_S ≤ 𝓘 (ord_le_one_of_idealSheaf_le, boClass_one_of_idealSheaf_le), the rounds
and the monomial phase are idle (stepACFunctor_seqOn_eq_nil), so the composite is the value of
the modified first step (composeOn_eq_of_firstList_eq_nil), which is the push-forward
(stepBFunctor_seqOn_eq_pushforwardRestrict_of_global).
Every level of the tower commutes with closed embeddings of empty divisor in codimension one
([Wlo09, §7.1], the passage to the hypersurface V(u₁); [Kol07, 34.3], [Kol07, 108]; the predicate
CommutesWithClosedEmbeddingsOfEmptyDivisorFam at s := 1): the level-n structure commutes
through the level-(n − 1) structure. Level n + 1 is
modFunctor_commutesWithClosedEmbeddings_one with R := the level-n functor (modTower_succ, by
definition); level 0 is the empty list on both sides (S = ∅ in dimension 0;
pushforwardRestrict_nil). Stated for BMOmodFamOfInput_of_hid, generic in the transform identity
hid, and with no hypothesis on bo and bmo, the argument being the construction's own descent.