Deleting empty blow-ups commutes with pull-back and push-forward #
The second clause of functoriality for smooth morphisms [Kol07, 34.1] compares two blow-up
sequences after "deleting every blow-up whose center is empty" (eraseEmpty), and the proof of
[Kol07, Lemma 102] says that for an arbitrary smooth h "the same blow-ups end up with empty
centers". To turn that sentence into equations one moves eraseEmpty past the three operations
that build the boundary-clearing sequence: the pull-back along a flat surjection, the pull-back
followed by a second deletion, and the push-forward along a closed immersion. This module proves
the three identities, all by induction on the sequence.
The center test. eraseEmpty (cons X D rest) tests D = ⊤ and, when it holds, carries the
deleted tail back to X along the inverse of the isomorphism D.blowUpπ
(isIso_blowUpπ_of_eq_top: the blow-up of the unit ideal). The lemma eraseEmpty_cons_of_eq_top
states this branch for any center D with a proof of D = ⊤, so that pulled-back and
pushed-forward centers (D.comap h, Z.map j), which are only propositionally equal to ⊤, need
no transport of types.
The identities. A flat surjection h preserves emptiness of centers both ways
(eq_top_of_comap_eq_top_of_surjective), and the inverse isomorphisms of the trivial blow-ups
intertwine with blowUpMap (inv_blowUpπ_comp_blowUpMap: both compose to the same map to X),
so eraseEmpty (S.pullback h) = (eraseEmpty S).pullback h
(eraseEmpty_pullback_of_flat_surjective). For an arbitrary h a nonempty center may pull back
to ⊤; deleting before or after the pull-back gives the same deleted sequence
(eraseEmpty_pullback_eraseEmpty'), the isomorphism case reducing to the surjective lemma. A
closed immersion preserves emptiness both ways (map_top, comap_map_of_isClosedImmersion), and
the square of a trivial blow-up is cartesian because its vertical maps are isomorphisms
(IsPullback.of_vert_isIso), so pullback_pushforward_of_isPullback_of_flat of
Hironaka/Scheme/BlowUpSequence/Pushforward.lean gives
eraseEmpty (S.pushforward j) = (eraseEmpty S).pushforward j (eraseEmpty_pushforward).
The blow-up of a center equal to the unit ideal is an isomorphism [Kol07, Warning 20].
The deletion of an empty first blow-up, for a center only propositionally equal to ⊤
(eraseEmpty_cons_top without a transport of the tail's type).
The inverses of two trivial blow-ups intertwine h with blowUpMap (both composites are the
same map to X, by blowUpMap_π).
The map of blow-ups over a flat h is flat (base change).
The map of blow-ups over a flat surjection is surjective (base change).
Deleting empty blow-ups commutes with pull-back along a flat surjection: a center is ⊤ iff
its inverse image is (the first clause of [Kol07, 34.1] is a statement without deletions).
Deleting the empty blow-ups before pulling back along any h does not change the deleted
pull-back (the second clause of [Kol07, 34.1]; "the same blow-ups end up with empty centers" in
the proof of [Kol07, Lemma 102]): the pulled-back center of a deleted step is ⊤.comap h = ⊤,
and the deletion commutes with the isomorphisms inv (blowUpπ _ ⊤)
(eraseEmpty_pullback_of_flat_surjective on an isomorphism); the statement assumes no flatness
of h.
Deleting empty blow-ups commutes with the push-forward along a closed immersion
([Kol07, 30.3] with the convention of [Kol07, 32]): a center is ⊤ iff its image is, and the
square of a trivial blow-up is cartesian (pullback_pushforward_of_isPullback_of_flat).
Deleting the empty blow-ups of the tail first does not change the deleted sequence
(eraseEmpty_eraseEmpty).