The transforms of a triple and the triples induced along a sequence #
Kollár's Definition 65 transforms a triple (X, I, E) under a smooth blow-up of order m with
center Z into (B_Z X, π_*^{-1} I, π_tot^{-1}(E)), and Definition 66 iterates this along a
smooth blow-up sequence of order m into (X_i, I_i, E_i); likewise for marked triples
[Kol07, Definitions 65 and 66]. The underlying data are the recursions weakTransform,
markedTransform, totalTransform and their sequence versions; this module proves that they
satisfy the conditions of [Kol07, Notation 64] and packages them as the triples
Triple.transform, MarkedTriple.transform, Triple.induced and MarkedTriple.induced.
The conditions, one by one. Finite type, quasi-compactness and separatedness of
B_Z X → Spec k come from the properness of the blow-up over a locally Noetherian X (finite
type over a field), composed with those of X; along a sequence every Π_i is proper, by
induction (isProper_stageMap, BlowUpSequence.isProper_composite). Smoothness and
equidimensionality are Kollár's Notation 19 for a smooth center of any shape
(Hironaka/Scheme/BlowUpSequence/SmoothCenter.lean), along a sequence by
IsSmooth.smoothOfRelativeDimension_stageMap. Nonvanishing on the components is preserved
(Hironaka/Scheme/BlowUpSequence/InducedData.lean). The total transform of a simple normal crossing
family under a blow-up whose center has simple normal crossings with it is again a simple normal
crossing family ([Kol07, Definition 25]; [Hau14, Proposition 5.3]), assembled here from the local
normal crossing data at the points of the exceptional divisor and off it and from the smoothness
of every member (Hironaka/Scheme/Snc/TotalTransformSnc.lean, TotalTransformOffCentre.lean);
along a sequence by induction with condition (3) of Definition 66 at every stage.
The total transform of a simple normal crossing family is simple normal crossing #
Properness of the stage maps, snc of the induced families #
Every composite Π_i of a blow-up sequence on a locally Noetherian scheme is proper (the
blow-up of a locally Noetherian scheme is proper, and proper morphisms compose).
The composite Π : X_r ⟶ X of a blow-up sequence on a locally Noetherian scheme is proper
(isProper_stageMap at the last index); for X of finite type over a field this is the
properness of a resolution [Kol07, (2)].
Along a smooth blow-up sequence of order m starting with (X, I, E), every induced family
E_i is simple normal crossing: condition (3) of [Kol07, Definition 66] iterated with
AlgebraicGeometry.totalTransform_isSnc.
Along a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), every induced
family E_i is simple normal crossing: condition (3′) of [Kol07, Definition 66] iterated.
The transformed and the induced triples #
The birational transform π_*^{-1}(X, I, E) = (B_Z X, π_*^{-1} I, π_tot^{-1}(E)) of a triple
under a smooth blow-up of order m with center Z [Kol07, Definition 65].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The birational transform π_*^{-1}(X, I, m, E) = (B_Z X, π_*^{-1}(I, m), π_tot^{-1}(E)) of a
marked triple under a smooth blow-up with center Z and ord_Z I ≥ m [Kol07, Definition 65].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triple (X_i, I_i, E_i) induced at stage i of a smooth blow-up sequence of order m
starting with T [Kol07, Definition 66, condition (1)]; Kollár's Π_*^{-1}(X, I, E) is its value
at Fin.last S.length.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The marked triple (X_i, I_i, m, E_i) induced at stage i of a smooth blow-up sequence of
order ≥ m starting with T [Kol07, Definition 66, condition (1′)].
Equations
- One or more equations did not get rendered due to their size.