Functoriality for smooth morphisms: blow-up sequence functors and pullback #

A blow-up sequence functor B commutes with a smooth morphism h : Y → X when B(Y, h^* I, h^{-1}(E)) = h^* B(X, I, E), and it commutes with smooth morphisms when it commutes with every smooth surjection and, for every smooth h, B(Y, h^* I, h^{-1}(E)) is the pull-back h^* B(X, I, E) with its empty blow-ups deleted [Kol07, 34.1]. The predicates are AlgebraicGeometry.Triple.IsPullbackOf T' T h (the triple T' carries the pullback data of T along h) and, on the functors of Hironaka/Scheme/BlowUpSequence/Functor.lean, CommutesWith, CommutesWithSmoothSurjections, CommutesWithSmooth (Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean). This module proves the basic facts about them.

Pullback data (isPullbackOf_pullback, IsPullbackOf.comp): the pullback of a triple (Hironaka/Scheme/BlowUpSequence/Pullback.lean) carries the pullback data by construction (its ambient scheme is Y, its ideal and family the inverse images, h over Spec k by hypothesis), and pullback data compose along f ≫ g because comap does (comap_comp; DivisorFamily.comap_comp componentwise).
Commuting with the identity and with composites (commutesWith_id, commutesWith_comp): the functoriality of the pull-back h^* of [Kol07, 30.1] (pullback_id, pullback_comp).
The two bullets (eraseEmpty_pullback_of_surjective, commutesWithSmooth_iff): along a smooth surjection the pulled-back value has no empty blow-ups (its centers are the inverse images of the nonempty centers under the stage lifts, which are surjective by base change, and the inverse image of a nonempty closed subscheme under a surjection is nonempty), so the second bullet of [Kol07, 34.1] implies the first.
Locality (eq_of_pullback_of_covers, eq_of_pullback_openCover, commutesWith_of_openCover, commutesWith_of_surjective_comp): two blow-up sequences agreeing after pullback to every member of a covering family of open immersions are equal, by induction on the sequence: the first centers agree because ideal sheaves are determined by their stalks (ext_stalkIdeal) and an open immersion is an isomorphism on stalks; the tails are pulled back along the lifted family blowUpMap (g i) D, again open immersions covering the blow-up (isPullback_blowUpMap, range_fst_of_isPullback). The nonempty index type is needed: on the empty scheme, sequences of every length have the same vacuous pullbacks along an empty cover. The surjective form is pullback_injective_of_surjective with pullback_comp. This is Kollár's remark that the functoriality isomorphism is unique when it exists, so that its existence is a local question [Kol07, 34].
The order predicates along pullback data (IsPullbackOf.isOrderSeq_pullback and the three related lemmas): the transport of the order conditions along a pullback in the form needed when one holds the pulled-back triple: the equidimensionality of T' (T'.smoothOfRelativeDimension, transported along h ≫ f = f') replaces the relative dimension of h, through the _of_equidim forms in PullbackInduced.lean, PullbackSnc.lean and PullbackEraseEmpty.lean.