Theorem 103 (3) in the compatible-family form #
Clause (3) of [Kol07, Theorem 103]: for a smooth hypersurface τ : Y ↪ X and an ideal sheaf
J ⊂ 𝒪_Y, nonzero on every component of Y, with τ_*(𝒪_Y / J) = 𝒪_X / I, one has
max-ord I = 1 and BO_{n,1}(X, I, ∅) = τ_* BMO_{n-1,1}(Y, J, 1, ∅). Kollár proves it in
[Kol07, 104, Step 2.4]: I contains the local equations of Y, so it has order 1 and
I = W(I); with E = ∅ Step 2.1 does nothing, in Step 2.2 one may choose H = Y, and the
statement follows from Lemma 102 (3). This module proves the analytic form for the construction
BO.BOanFamOfInput of BOanFamOfInput.lean, on every relatively compact open subset, with the
marked family of dimension n - 1 at the mark 1 in the role of BMO_{n-1,1}: the predicate
CommutesWithClosedEmbeddingsOfEmptyDivisorFam of Functor/FamilyClosedEmbedding.lean asks that
the value on (M, 𝓘, ∅) over U be the push-forward of the value on (Y, τ^* 𝓘, ∅) over the
trace U ∩ Y. The finite counterpart is ClosedEmbedding.lean.
The argument follows Kollár's step by step.
- The triple
(M, 𝓘, ∅)lies inLocalMCClass 1withH := Y, since the ideal sheaf ofYlies in𝓘 = D⁰ 𝓘; the value of the construction, the descent of the local family functor along a cover by pieces with maximal contact (GlobalizeFam.lean), is therefore the local functor's own value (globalizeFam_fam_eq), and no cover enters. - At the mark
1the tuning is the identity (AnalyticTriple.tuned_one), and the hypersurface of maximal contact chosen from the class may be replaced byY(hfStep2SeqFamOn_indep, the independence of Step 2.3). - Step 2.1 is idle on the empty boundary. To see it, the list of nonempty boundary members is made
a parameter of Step 2 along the chain of opens (
hfStep2SeqFamAlongList): over the empty list the chain of Step 2.1 is its initial state, and the value of Step 2 onUis the value of Step 2.2 alone (shrinkAppend_nil), Lemma 102's family at the single memberYof∅ + Y, read on the reading open of the chain and carried to an open ofMby the commutation of the Step 2.2 functor with local analytic isomorphisms. - Lemma 102's family at the mark
1onY(BDanFam_one_eq_pushforwardRestrict): the first centreZ_{-1}is empty because𝓘|_Yis nonzero everywhere, so the first blow-up is empty and deleted, the push-forward is transported along the isomorphism of the empty blow-up, and the value of the input family on the restricted triple is its value on(Y, J, ∅)pulled back along the restricted isomorphism, by its commutation with local analytic isomorphisms and its indifference to empty members. - The push-forward over an open commutes with restriction to a smaller open ([Kol07, 30.3] on each
open;
pushforwardRestrict_pullback_restrictLE), and the compatibility of the input family carries its value from the trace of the larger open toU ∩ Y.
The result gives Theorem 103 (3) at every stage of the order-reduction tower
(Stage/AllNFam.lean) and enters the closed-embedding clause of the embedded desingularization
(Modified/ClauseClosedEmbedding.lean, Functor/ChainClosedEmbeddingZero.lean).
Step 2 along a chain, with the list of members as a parameter #
The state of the chain of Step 2.1 at the next-to-last open, over an arbitrary list l of
members of the boundary in place of the list of nonempty members (over data d).
Equations
- Hironaka.Manifold.BO.hfChainList T s hT W l hWsub d hW = Hironaka.Manifold.step21FamAux T s d.bd₁ hT W (l.length + 1) hW hWsub l ⋯
Instances For
Step 2 along a chain of opens with the list of members as a parameter (over data d):
hfStep2SeqFamAlong (Step2Along.lean) with the list of nonempty members of the boundary
replaced by l, so that the empty boundary can be substituted. The chain of Step 2.1 over l is
restricted to the last open, the value of Step 2.2 over its state (hfStep22ValueOf) is appended,
and the result is restricted to U with its empty blow-ups deleted.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Step 2 along a chain is Step 2 along the chain over the list of nonempty members, by definition.
The value depends on the list only; the hypotheses on the chain are transported.
The push-forward over an open under restriction and deletion of empty blow-ups #
The trace on a closed submanifold of a smaller open is smaller.
The push-forward of a sequence of centres depends only on the set of the closed submanifold and on the sequence.
The push-forward over an open commutes with restriction to a smaller open ([Kol07, 30.3] on
each open): the push-forward over V of a sequence on the trace V ∩ S, restricted to U ≤ V, is
the push-forward over U of the sequence restricted to the trace U ∩ S.
The push-forward over an open, unfolded: the sequence on the trace U ∩ S is carried by the
isomorphism between the trace and the closed submanifold S ∩ U of M|_U, then pushed forward.
The push-forward over an open of a sequence without empty centres has none ([Kol07, 32]).
Up to the deletion of empty blow-ups, the push-forward over an open does not see the empty blow-ups of the sequence.
Lemma 102's family at the mark 1 on a member with empty first centre #
Lemma 102 (3) in the compatible-family form ([Kol07, Lemma 102 (3)], as used in
[Kol07, 104, Step 2.4]): at the mark 1, on a member Y of the boundary all of whose other
members are empty, with J := 𝓘|_Y nonzero everywhere, the value of Lemma 102's family at Y on
U is the push-forward over U of the value of the input family on (Y, J, ∅) over the trace
U ∩ Y. The first centre Z_{-1} is empty (Zminus1_one_eq_empty_of_isNonzeroEverywhere), so the
first blow-up is empty and deleted and the push-forward is transported along the isomorphism of
the empty blow-up; the value of the input family on the restricted triple is its value on
(Y, J, ∅) pulled back along the restricted isomorphism, by its commutation with local analytic
isomorphisms and its indifference to empty members (the restricted boundary is empty), the ideal
sheaves agreeing because the weak transform by an empty blow-up is the pull-back
(weakTransformI_eq_comap_of_eq_empty) and restriction commutes with pull-back
(pullback_inclusionMap_pullback).
Step 2 at the mark 1 along a global hypersurface #
Step 2 at the mark 1 along a global hypersurface of codimension one, over data d
([Kol07, 104, Step 2.4]; [Wlo09, §7.1]): on (M, 𝓘 ⊇ I_S, ∅) with S a closed hypersurface, if
the family functor of Step 2.2 at the triple of Step 2.2 over the empty sequence is, on every
relatively compact open, the push-forward of a compatible family C on S, then Step 2 on the
tuned triple is the push-forward of C on U. The tuning is the identity at the mark 1
(tuned_one, hfStep2FamOn_congr_triple), the class's chosen hypersurface is replaced by S
(hfStep2SeqFamOn_indep), Step 2.1 is idle on the empty boundary (the list-parametrised chain at
[], shrinkAppend_nil), and Step 2.2 is read on the chain's open and carried to U
(hfStep22Functor_commutesWithLocalIsos, pushforwardRestrict_pullback_restrictLE, the
compatibility of C).
Theorem 103 (3) for the construction #
Theorem 103 (3) in the compatible-family form ([Kol07, Theorem 103 (3)], proved as in
[Kol07, 104, Step 2.4]): the order-reduction structure BO.BOanFamOfInput 𝕜 n inp at the mark 1
commutes with closed embeddings of hypersurfaces when the boundary is empty, through the input
marked family inp 1 of dimension n - 1 at the mark 1: for a closed hypersurface S ⊆ M, an
ideal sheaf 𝓘 containing the ideal sheaf of S and J = 𝓘|_S, the value on (M, 𝓘, ∅) over a
relatively compact open U is the push-forward over U of the value of inp 1 on (S, J, ∅) over
the trace U ∩ S. The triple (M, 𝓘, ∅) has the global hypersurface of maximal contact S, so
the value is the local functor's, Step 2 at the mark 1 along S
(hfStep2FamOn_eq_pushforwardRestrict_of_global); Step 2.2 there is Lemma 102's family at the
member S, the push-forward of the input's value (BDanFam_one_eq_pushforwardRestrict).