The boundary of a blow-up sequence as a simple normal crossing family #
The boundary E_i of a sequence Π starting with the empty boundary (boundarySeq from
⊤) is defined by the recursion E_{i+1} = red(π_i⁻¹(E_i) ∪ π_i⁻¹(Z_i))
(reducedTransform), the recursion of the analytic main theorem
[Hir64, Main Theorem II′(N), clause (iii), p. 156]. Kollár works instead with the ordered family
of the exceptional divisors [Kol07, Definition 25]: F_0 = ∅, and F_{i+1} is the total
transform of F_i by π_i, the strict transforms of the components followed by the new
exceptional divisor (HypersurfaceFamily.totalTransform). This module defines that family along
the sequence (totalTransformSeq, by recursion on the stage; more generally
totalTransformSeqFrom from an arbitrary start family) and proves, for a sequence of order ≥ m
(IsOfOrderGe, whose clause (3′) says that E_i has only normal crossings with Z_i), that
F_i is a simple normal crossing family with E_i its reduced ideal sheaf at every stage
(boundarySeq_eq_idealSheaf_totalTransformSeq), and that the centre Z_i has simple normal
crossings with F_i in the chart sense of [Kol07, Definition 24 (4)]
(hasSncWith_totalTransformSeq_center). Induction on the stage: the stalk clause (3′) is the
chart clause "Z_i has simple normal crossings with F_i" by the dictionary
hasOnlyNormalCrossingsWith_idealSheaf_iff; isSnc_totalTransform makes F_{i+1} a simple
normal crossing family, and reducedTransform_eq_idealSheaf_totalTransform identifies
red(π_i⁻¹E_i ∪ π_i⁻¹Z_i) with its reduced ideal sheaf. Each statement also comes in a
prefix-bounded form (…_of_forall_lt) assuming clause (3′) only at the stages before the one
considered, for the joint inductions in which clause (3′) of a sequence is itself being proved.
The two descriptions of the boundary bridge the stalk-local normal-crossings clause of the main theorems and Kollár's chart-wise simple normal crossings; both are used throughout the going-up and order-reduction arguments.
The reduced ideal sheaf of the empty divisor is the unit ideal sheaf.
The family of exceptional divisors along the sequence from a start family F
[Kol07, Definition 25], by recursion on the stage: F_0 = F, and F_{i+1} is the total transform
of F_i under π_i with centre Z_i. The empty start is totalTransformSeqAux.
Equations
- S.totalTransformSeqFromAux F 0 x_2 = F
- S.totalTransformSeqFromAux F i.succ h = Manifold.HypersurfaceFamily.totalTransform (⇑(S.map ⟨i, ⋯⟩)) (Manifold.IdealSheaf.support (S.center ⟨i, ⋯⟩)) (S.totalTransformSeqFromAux F i ⋯)
Instances For
The boundary family at stage i starting from F.
Equations
- S.totalTransformSeqFrom F i = S.totalTransformSeqFromAux F ↑i ⋯
Instances For
The family of exceptional divisors at stage i [Kol07, Definition 25], by recursion on the
stage: F_0 = ∅, and F_{i+1} is the total transform of F_i under π_i with centre Z_i (the
strict transforms of the components of F_i followed by π_i⁻¹(Z_i)).
Equations
Instances For
The family F_i of exceptional divisors on the stage X_i [Kol07, Definition 25].
Equations
- S.totalTransformSeq i = S.totalTransformSeqAux ↑i ⋯
Instances For
The empty start is the family of exceptional divisors, definitionally.
The boundary recursion, one step (definitional).
The comparison of Kollár's family of exceptional divisors [Kol07, Definition 25] with the
reduced boundary of [Hir64, Main Theorem II′(N), p. 156], from a start family and in
prefix-bounded form: for a simple normal crossing start F, under clause (3′) for the boundary
starting with red F at the stages < i, the family F_i from the start F is a simple normal
crossing family at stage i and the boundary E_i is its reduced ideal sheaf. Induction on the
stage: clause (3′) at a stage says that E_i has only normal crossings with Z_i, which by the
dictionary hasOnlyNormalCrossingsWith_idealSheaf_iff is "Z_i has simple normal crossings with
F_i"; isSnc_totalTransform makes F_{i+1} a simple normal crossing family and
reducedTransform_eq_idealSheaf_totalTransform identifies red(π_i⁻¹E_i ∪ π_i⁻¹Z_i) with the
reduced ideal sheaf of the total transform. The start enters only through E_0 = red F, so the
base case is rfl. Not in the sources in this form.
The form of hasSncWith_totalTransformSeq_center from a start family: clause (3′) for the
boundary starting with red F at the stages ≤ i gives Kollár's chart-wise clause at stage i,
that Z_i has simple normal crossings with F_i.
The prefix-bounded form of isSnc_totalTransformSeq_and_boundarySeq_eq, for the joint
inductions that prove clause (3′) of a transformed sequence (a restriction or push-forward in the
sense of [Kol07, Definition 30]): the conclusion at stage i uses clause (3′) of Π at the
stages < i only, and the order clause never enters.
For a sequence of order ≥ m with the empty boundary, the family F_i of exceptional
divisors [Kol07, Definition 25] is a simple normal crossing family at every stage, and the
boundary E_i of the recursion of [Hir64, Main Theorem II′(N), p. 156] is its reduced ideal sheaf.
Induction on the stage: clause (3′) of Π at stage i says that E_i has only normal crossings
with Z_i, which by the dictionary is "Z_i has simple normal crossings with F_i";
isSnc_totalTransform then makes F_{i+1} a simple normal crossing family and
reducedTransform_eq_idealSheaf_totalTransform identifies red(π_i⁻¹E_i ∪ π_i⁻¹Z_i) with the
reduced ideal sheaf of the total transform.
The prefix-bounded form of isSnc_totalTransformSeq.
The family of exceptional divisors of a sequence of order ≥ m is a simple normal crossing
family at every stage.
The prefix-bounded form of boundarySeq_eq_idealSheaf_totalTransformSeq.
The boundary of a sequence of order ≥ m with the empty boundary is the reduced ideal sheaf
of its family of exceptional divisors.
The prefix-bounded form of hasSncWith_totalTransformSeq_center: clause (3′) of Π at the
stages ≤ i gives Kollár's chart-wise clause at stage i.
Clause (3′) of a sequence of order ≥ m in Kollár's form: the centre Z_i has simple normal
crossings with the family of exceptional divisors F_i [Kol07, Definition 24 (4)].