The boundary of the restricted succession is the trace #
Kollár restricts a smooth blow-up sequence Π with centres Z_i ⊆ S_i to the strict transforms
S_i of a closed submanifold S [Kol07, Definition 30.2] (restrictSubmanifold, whose stages are
the S_i and whose blow-downs are the restrictions of the π_i). This module proves the
set-theoretic half of the normal-crossings clause (3′) of [Kol07, Definition 66] for Π|_S: the
support of the boundary E'_i of Π|_S (boundarySeq from the unit ideal sheaf) is the trace
E_i ∩ S_i of the boundary of Π — the preimage of supp E_i under the inclusion S_i ↪ X_i
(support_boundarySeq_restrictSubmanifold). Induction on the stage: both boundaries start empty,
and reducedTransform_support reads the recursion E_{i+1} = red(π_i⁻¹E_i ∪ π_i⁻¹Z_i) on the
supports (the reduced analytic subspace red(f⁻¹(E) ∪ f⁻¹(D)) of Hironaka's analytic theorem,
[Hir64, Ch. 0, §7, Main Theorem II′(N)]), where the centres of Π|_S are the traces of the centres
(support_center_restrictSubmanifold) and the blow-downs commute with the inclusions
(restrictIncl_map). The proper invariant of Snc/Proper.lean is carried along the succession
(hasSncWithProper_totalTransformSeq_strictTransformSeq: S_i has simple normal crossings with
the boundary family F_i, properly, at every stage — vacuous at stage 0 and transported by each
blowing-up through hasSncWithProper_totalTransform, the centre Z_i ⊆ S_i having simple normal
crossings with F_i by clause (3′) of Π). The prefix-bounded forms (clause (3′) assumed only at
the stages < i) and the forms with an arbitrary starting boundary family F serve the lifting of
simple normal crossings along the restriction. Not in the sources; routine.
The support of the boundary of Π|_S started with E₀' is the trace of the support of the
boundary of Π started with E₀, at every stage, as soon as it is at stage 0 — the recursion is
start-agnostic (support_boundarySeq_restrictSubmanifold is the unit start; the traces of
[Kol07, Definition 30.2] on the supports).
The boundary of the restricted succession Π|_S, started with the unit ideal sheaf, has as
support the trace of the boundary of Π at every stage — supp E'_i = S_i ∩ supp E_i, read as the
preimage under the inclusion S_i ↪ X_i ([Kol07, Definition 30.2] on the supports).
The prefix-bounded form of hasSncWithProper_totalTransformSeq_strictTransformSeq — clause
(3′) of Π at the stages < i suffices for the proper invariant at stage i.
Along a succession of order ≥ m with centres Z_i ⊆ S_i [Kol07, Definition 30.2], the strict
transform S_i has simple normal crossings with the boundary family F_i, properly (no component
of F_i contains S_i near any point), at every stage. Induction on the stage: vacuous for the
empty family at stage 0; the step is the transport of the proper invariant by the blowing-up π_i
along Z_i ⊆ S_i (hasSncWithProper_totalTransform), with Z_i having simple normal crossings
with F_i by clause (3′) of Π (hasSncWith_totalTransformSeq_center). No clopen argument on the
components enters: the trace of a component on S_i is a hypersurface of S_i by the invariant at
each point.
The trace of the boundary family on the stages of the restriction #
The trace on S_i of the boundary family from the start F, typed on the stages
finStages.
Equations
- S.traceFamilyFromAux hH hc F 0 hi = ⋯.traceFamily (S.totalTransformSeqFromAux F 0 hi)
- S.traceFamilyFromAux hH hc F i.succ hi = ⋯.traceFamily (S.totalTransformSeqFromAux F (i + 1) hi)
Instances For
The trace on S_i of the boundary family F_i from the start F (Kollár's E_i ∩ S_i
[Kol07, Definition 30.2] with the boundary E = red F).
Equations
- S.traceFamilyFrom hH hc F i = S.traceFamilyFromAux hH hc F ↑i ⋯
Instances For
The trace of the boundary family F_i on the stage S_i of Π|_S, typed on the stages
finStages (as restrictCenterAux) — the empty start of traceFamilyFromAux.
Equations
- S.traceFamilyAux hH hc = S.traceFamilyFromAux hH hc (Manifold.HypersurfaceFamily.empty M.carrier)
Instances For
Kollár's boundary E_i ∩ S_i [Kol07, Definition 30.2] as a family of hypersurfaces of S_i:
the trace of the boundary family F_i on the stage S_i of Π|_S.
Equations
- S.traceFamily hH hc i = S.traceFamilyAux hH hc ↑i ⋯
Instances For
The support of the trace family is the trace of the support of F_i.
The support of the trace family from F is the trace of the support of F_i.
The prefix-bounded form of isSnc_traceFamily.
The trace of the boundary family on S_i is a simple normal crossings divisor of S_i —
S_i has simple normal crossings with F_i properly along Π.
The prefix-bounded form of support_traceFamily_eq_support_boundarySeq.
The support of the trace family is the support of the boundary of Π|_S.
The prefix-bounded form of stalkIdeal_boundarySeq_restrictSubmanifold.
The boundary of Π|_S is the reduced ideal sheaf of its support at every stage — the unit
ideal sheaf at stage 0, and at a later stage the red branch of the recursion (Hironaka's reduced
analytic subspace, [Hir64, Ch. 0, §7, Main Theorem II′(N)]), the vanishing ideals of
supp E'_i = |E_i ∩ S_i| having local generators because the trace family has simple normal
crossings.
The prefix-bounded form of boundarySeq_restrictSubmanifold_eq_idealSheaf_traceFamily — the
input of the lifting of simple normal crossings along the restriction.
The boundary of Π|_S is the reduced ideal sheaf of the trace of the boundary family — both
are the reduced ideal sheaves of the same set |E_i ∩ S_i|.
The trace of the boundary family from F on S_i has simple normal crossings when F_i has
and has simple normal crossings with S_i properly (isSnc_traceFamily is the empty start).
The base identity of the supports for the start E = red F on M and E|_S = red (F|_S) on
S, for F snc having simple normal crossings with S properly.
The support of the trace family from F is the support of the boundary of Π|_S started
with E|_S = red (F|_S), under clause (3′) at the stages < i.
The boundary of Π|_S started with E|_S = red (F|_S) is the reduced ideal sheaf of its
support at every stage — at stage 0 because F|_S has simple normal crossings, at a later stage
the red branch of the recursion ([Hir64, Ch. 0, §7, Main Theorem II′(N)]), the vanishing ideals
of |E_i ∩ S_i| having local generators because the trace family from F has simple normal
crossings (the proper invariant hprop at the stages ≤ i).
The boundary of Π|_S started with E|_S is the reduced ideal sheaf of the trace of the
boundary family from F — both are the reduced ideal sheaves of the same set (Kol07, Definition
30.2 with the boundary E = red F).
The normal-crossings clause (3′) of [Kol07, Definition 66] for Π|_S: along a succession of
order ≥ m with the empty boundary and centres Z_i ⊆ S_i, the boundary E'_i of the restricted
succession Π|_S has only normal crossings with its centre Z_i ∩ S_i at every stage. Proof:
E'_i is the reduced ideal sheaf of the trace family
(boundarySeq_restrictSubmanifold_eq_idealSheaf_traceFamily), the centre of Π|_S is the ideal
sheaf of the closed submanifold Z_i ∩ S_i of S_i (restrictCenterSub'), and the dictionary
hasOnlyNormalCrossingsWith_idealSheaf_iff reduces clause (3′) to "Z_i ∩ S_i has simple normal
crossings with the trace family" (hasSncWith_traceFamily, from a chart adapted simultaneously to
the centre, the submanifold and the family).