The nerve transition: the geometric transition realises the combinatorial one #
The central fact of the geometric realisation of [Kol07, 111, Step 3]: after blowing up a centre
S of the state, the nerve of the transported piece family blowUpPieces is the nerve
MonomialState.blowUpNerve that the combinatorial transition prescribes
(nerve_blowUpPieces), so that the state of the transported family is the combinatorial
transition of the state, a literal equality (toState_blowUpPieces), and the transported
family realises the total transform of the boundary through the extended label isomorphism
(realizes_blowUpPieces). Not in the sources; Kollár describes the new r-fold intersections
in one sentence of [Kol07, 111, Step 3.r]: they are the E^{i₁} ∩ ⋯ ∩ E^{i_{r-1}} ∩ E^{j_ℓ} with
E^{i₁} ∩ ⋯ ∩ E^{i_{r-1}} ≠ ∅.
On a smooth k-scheme X, for the blow-up π : B_Z X → X of a centre Z = centerOf S of the
state, three set-level facts are proved first:
faceSet_blowUpPieces_of_mem: the strict transforms of the pieces of a facePof the centre have empty common intersection. A common pointx'lies overx ∈ Z_P, on the exceptional divisor; by Nakayama (exists_stalkIdeal_comap_eq_span_of_mem_supportofHironaka/Resolution/Algebraic/Monomial/Geometric/Chart.lean) someπ^* z_c,cthe coordinate of a piece ofP, generates the exceptional ideal atx', and then the strict transform of that piece missesx'(Hironaka/Scheme/Snc/TotalTransformSnc.lean).faceSet_blowUpPieces_ne_bot_iff: a nonempty set of old pieces has nonempty intersection after the blow-up iff it had one before and contains no face of the centre. The existence half uses the origin of a chart (exists_π_eq_mem_faceSet_blowUpPieces).faceSet_blowUpPieces_insert_newComp_ne_bot_iff: the new pieceF_P = π⁻¹(Z_P)meets the strict transforms of the old piecesT₁iffT₁ ∪ Pis a face andP ⊄ T₁.
A face of the new family contains at most one new piece, two new pieces π⁻¹(Z_P),
π⁻¹(Z_Q) being disjoint, and the last two facts identify the faces without and with a new
piece. The module also records piece death (blowUpPieces_piece_eq_bot_iff: an old piece
disappears exactly when its singleton is a face of the centre, the trivial blow-up of
[Kol07, Warning 20]) and the bridge strictTransformCloseds_eq_support between the closed-set
and the ideal-sheaf strict transforms. The results are used along the whole run in
Hironaka/Resolution/Algebraic/Monomial/Geometric/Realize.lean.
The set/ideal bridge #
The strict transform of a closed set (the closure of π⁻¹(C ∖ Z)) is the support of the
strict transform of its vanishing ideal (coe_support_strictTransform of
Hironaka/Resolution/Algebraic/Snc/DictionaryBoundary.lean, on the locally Noetherian X).
The family of the pieces' vanishing ideals, indexed by the live components.
Equations
Instances For
Kollár's snc data (the hypothesis of Hironaka/Scheme/Snc/TotalTransformSnc.lean) for the
family of the pieces' vanishing ideals at a point of the centre of a centre of the state: the pieces
through the point have distinct labels, hence distinct members and distinct coordinates.
The strict transforms of a face of the centre have empty intersection #
The strict transforms of the pieces of a face of the centre have empty common intersection:
a common point lies over a point of Z_P, on the exceptional divisor; some coordinate z_c of
a piece of P generates the exceptional ideal there (Nakayama), and the strict transform of
that piece misses the point.
Points over the pieces: the image of a point of a strict transform #
A point of the strict transform of a piece lies over a point of the piece.
A point of the intersection of the strict transforms of old pieces lies over a point of their intersection.
Two pieces through a point with the same stalk ideal coincide #
Two pieces through x whose vanishing ideals have the same stalk at x coincide: pieces of one
label through x coincide (Realizes.disjoint), and two members through x have distinct
coordinates, hence distinct stalk ideals (IsSncAt, in the regular local ring 𝒪_{X,x}).
A generator of the exceptional ideal is a regular parameter #
At a point of the exceptional divisor over the centre of a centre of the state, a generator
of the exceptional ideal does not lie in 𝔪²: the exceptional ideal is (z'_j) for a regular
system of parameters z' (Hironaka/Scheme/Snc/TotalTransformData.lean).
The witness over a point of the center: the origin of a chart #
The existence half of the nerve transition at a point x of Z_Q (Q a face of the
centre): for a set T of old pieces through x missing some piece kc of Q, the origin of the
chart of kc's coordinate lies over x on the strict transform of every piece of T.
Transversal pieces (coordinate not among those of Z) contain the whole fibre, and for a piece
c ∈ Q ∖ {kc} the strict transform has stalk (u) with π^* z_c = u · π^* z_{kc}, where u
is not a unit since π^* z_c ∈ 𝔪² at the origin while π^* z_{kc}, a generator of the
exceptional ideal, is not.
The faces without and with a new piece #
A nonempty set T of old pieces has nonempty intersection after the blow-up iff it had one
before and contains no face of the centre.
The new piece F_P = π⁻¹(Z_P) meets the strict transforms of the old pieces T₁ iff
T₁ ∪ P is a face and P ⊄ T₁.
The nerve transition #
Membership in a new piece: the point lies over Z_P for the face P allocated to the index.
The nerve transition: the nerve after the blow-up of a centre of the state is
MonomialState.blowUpNerve of the nerve. A face of the new family contains at most one new
piece (two new pieces π⁻¹(Z_P), π⁻¹(Z_Q) are disjoint), and
faceSet_blowUpPieces_ne_bot_iff and faceSet_blowUpPieces_insert_newComp_ne_bot_iff identify
the faces without and with a new piece.
The transported family is valid and its state is the transition #
The transported family's data are Valid: they are the data of the state blowUp S, whose
invariants are proved in Hironaka/Resolution/Algebraic/Monomial/State.lean.
The transported piece family's state is the combinatorial transition of the state, a
literal equality of MonomialStates.
Piece death #
A generic point of a piece is a generic point of the support of its member: a point of the member generizing it lies on a piece of the same label, which is the piece itself (two pieces of one label being disjoint).
Through a generic point of a piece passes no other piece: a piece of the same label is the
piece itself, and no other member passes through a generic point of a component
(notMem_support_of_ne of Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean).
Piece death (the trivial blow-up of [Kol07, Warning 20]): a nonempty piece lies in the centre iff its singleton is a face of the centre. At a generic point of the piece only that piece passes, so the face of the centre through it is the singleton.
Piece death: the strict transform of an old piece is empty iff the piece was empty or its singleton is a face of the centre.
The transported family realizes the total transform #
The old pieces of the transported family with a given label below nextLabel are the old
pieces of that label.
The pieces of the transported family with the new label are the new pieces.
The transported piece family realises the total transform π^{-1}_{tot} E of
[Kol07, Definition 65] through the extended label isomorphism: the strict transform of a member
is the union of the strict transforms of its pieces (closure commutes with finite unions), the
exceptional divisor is the union of the new pieces π⁻¹(Z_P), and pieces of one label stay
disjoint.