The disjoined triple (X', π^* I, E^0 + E^1 + ⋯ + E^{k-1}) #
After the k − 1 disjoining steps "we get rid of all pairwise intersections as well"
[Kol07, 72]: the end result is π : X' → X with E^0 := π^{-1}_*(E_1 + ⋯ + E_k) a smooth
divisor, and with E^1, …, E^{k-1} the birational transforms of the exceptional divisors
F^1, …, F^{k-1}, the triple (X', π^* I, ∑_{i=0}^{k-1} E^i) satisfies the assumptions of
Theorem 68. The assumptions are those of a triple
[Kol07, Notation 64]: X' is smooth and equidimensional over k (along the sequence), π^* I is
nonzero on every component (the stalk maps of a smooth blow-up of a smooth scheme are injective:
over the center by the chart description of the blow-up, off it because the blow-up is a local
isomorphism), and the ordered family E^0 < E^1 < ⋯ < E^{k-1}, the total transform with the
birational transforms of the original components collapsed into E^0, is snc because those
transforms are pairwise disjoint (meetLocus_strictTransformSeq_disjoinSeq) and collapsing
pairwise disjoint components of an snc family gives an snc family (isSnc_collapse); E^0 is
then a smooth divisor.
isNonzeroEverywhere_comap_blowUpπ,isNonzeroEverywhere_comap_composite_of_isSmooth: the transport of "nonzero on every component" along smooth blow-ups (which are not flat, soisNonzeroEverywhere_comap_of_flatdoes not apply).disjoinedFamily_component_bot,disjoinedFamily_component_coe,card_disjoinedFamily: the shape of Kollár's family.disjoinedFamily_isSnc,isSmoothDivisor_disjoinedFamily_bot,smoothOfRelativeDimension_composite_disjoinSeq,isNonzeroEverywhere_comap_composite_disjoinSeq: the assumptions of Theorem 68.Hironaka.disjoinedTriple: the disjoined triple, the input of the marked order reduction functor in the construction of the principalization functor (Hironaka/Resolution/Algebraic/Kol07/Thm35/Principalization.lean).
The inverse image of an ideal sheaf nonzero on every component under a smooth blow-up of a smooth scheme is nonzero on every component (the condition on the ideal of a triple in [Kol07, Notation 64]): the stalk maps of the blow-up are injective (over the center by the chart description of the blow-up, an isomorphism off it).
Along a smooth blow-up sequence of a smooth scheme, the inverse image of an ideal sheaf nonzero on every component is nonzero on every component [Kol07, 72 and Notation 64].
E^0 = π^{-1}_*(E_1 + ⋯ + E_k) [Kol07, 72], the divisor of the final birational transforms of
the components.
"Let E^1, …, E^{k-1} denote the birational transforms of F^1, …, F^{k-1}" [Kol07, 72]: the
other components of the disjoined family are the remaining components of the total transform, in
its order.
The index set of the total transform at stage i has i more members than E.
The disjoined family has E^0 and one E^j per step [Kol07, 72].
∑_{i=0}^{k-1} E^i is a simple normal crossing divisor with the ordered index set
E^0 < ⋯ < E^{k-1} [Kol07, 72 and Notation 64].
"E^0 := π^{-1}_*(E_1 + ⋯ + E_k) is a smooth divisor" [Kol07, 72].
π^* I is nonzero on every component of X' [Kol07, 72 and Notation 64].
X' is smooth and equidimensional over k [Kol07, 72 and Notation 64].
The disjoined triple #
The disjoined triple (X', π^* I, ∑_{i=0}^{k-1} E^i) of [Kol07, 72], with π : X' → X
the disjoining sequence of T.E, π^* I its inverse image ideal sheaf and the ordered family
E^0 < E^1 < ⋯ < E^{k-1} of collapsedFamily; it "satisfies the assumptions of (68)".
Equations
- One or more equations did not get rendered due to their size.