Subdivisions of divisor families #
The refinement of a blow-up sequence to irreducible centers
(Hironaka/Resolution/Algebraic/Kol07/RefineIrreducible.lean) replaces the blow-up of a center Z = ⊔ Z_k by the componentwise sequence of its components, so
the exceptional divisor f⁻¹(Z) of the original sequence reappears in the refined one as the c
exceptional divisors of the components, and every later total transform of the refined sequence is
a subdivision of the corresponding total transform of the original: at each point, each of its
components has the stalk of a component of the original family, injectively. Kollár's simple
normal crossing condition [Kol07, Definition 24 (4)] only sees the components through a point and
their stalks, so it passes from a family to any subdivision (hasSncWith_of_subdivides), and with
it the order condition of [Kol07, Definition 66] (isOrderSeq_of_subdivides,
isOrderGeSeq_of_subdivides). This module sets up the relation and its stability under inverse
images, total transforms (the stalk of a strict transform depends only on the stalk of the
transformed ideal, the stalk formula for saturations) and open covers, and shows that a family
subdivides its collapse along pairwise disjoint members (subdivides_collapse).
The divisor family F subdivides G if at every point x there is an assignment q of
components of F to components of G, sending each component of F through x to a component
of G with the same stalk at x, injective on the components through x. The exceptional
divisor of the blow-up of a disjoint union ⊔ Z_k is subdivided by the exceptional divisors of the
Z_k. Not in the sources; the relation along which simple normal crossings are transported to the
refinement of a sequence to irreducible centers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A point with unit stalk ideal is off the support (the stalk ideal at a point of the support
lies in the maximal ideal, mem_support_iff_stalkIdeal_le_maximalIdeal).
Two ideal sheaves with the same stalk at x have x in both supports or in neither.
Every family subdivides itself.
Subdivisions compose.
Subdivisions pull back along any morphism: the components through y of the inverse image are
the inverse images of the components through g y (mem_support_comap_iff_apply), with the
mapped stalks (stalkIdeal_comap).
The subdivision relation is local: it holds as soon as it holds after restriction to the
members of an open cover (the stalks at ι w and at w correspond under the stalk isomorphism of
the open immersion, stalkIdeal_eq_map_symm_stalkIdeal_comap).
Simple normal crossings with Z [Kol07, Definition 24 (4)] pass from a family to any
subdivision of it: the components of the subdivision through x are assigned injectively to
components of the coarser family through x with the same stalks, so the same coordinates and the
composed assignment work.
Subdivisions are preserved by the total transform [Kol07, Definition 25] along a morphism π
with an invertible distinguished divisor K: a strict transform through y comes from a
component through π y, and the stalk of the strict transform ((I.comap π) : K^∞) at y
depends only on the stalk of I at π y (the stalk formula stalkIdeal_saturate_of_isInvertible);
the distinguished divisor is assigned to itself.
Subdivisions are preserved by the total transform under a blow-up [Kol07, Definition 25].
A smooth blow-up sequence of order d [Kol07, Definition 66] for the family E is one for
every subdivision F of E: stage by stage, the induced families of F subdivide those of E
(subdivides_totalTransform) and the snc conditions descend (hasSncWith_of_subdivides); the
smoothness and order conditions do not involve the family.
Subdivision by a collapse, and the marked form of isOrderSeq_of_subdivides #
A family subdivides its collapse along pairwise disjoint members (the collapse of the disjoint
members of the boundary into one divisor in the proof of [Kol07, Theorem 35] given in [Kol07, 72]):
a collapsed member is assigned to the collapsed divisor ⊥, whose stalk at a point is the stalk of
the one collapsed member through it (exists_stalkIdeal_prod_eq_of_disjoint); the other members
are unchanged.
The marked form of isOrderSeq_of_subdivides: a smooth blow-up sequence of order ≥ m
[Kol07, Definition 66] for the family E is one for every subdivision F of E. Stage by stage
the induced families of F subdivide those of E (subdivides_totalTransform) and simple normal
crossings descend (hasSncWith_of_subdivides); the smoothness and order conditions do not involve
the family.