Functoriality of BD_{n,m,j} under smooth morphisms #
Clause (2) of [Kol07, Lemma 102], the smooth part: for a smooth surjection h : Y → X, Kollár
notes that pulling back by h and then restricting to E^j_Y = h^{-1}(E^j) gives the same triple
as restricting to E^j and then pulling back by h|_{E^j_Y}, so the functoriality of
BMO_{n−1,m} gives h^* BD_{n,m,j}(X, I, E) = BD_{n,m,j}(Y, h^*I, h^{-1}E); for an arbitrary
smooth h "the same blow-ups end up with empty centers" ([Kol07, 34.1], the second bullet). This
module proves both for the construction of Restriction.lean and Output.lean (rawSeq,
functor), for a general pull-back pair T'.IsPullbackOf T h
(Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean) and the j-th members by POSITION
(pos T hj = monoEquivOfFin T.E.ι rfl ⟨j, hj⟩, so that T.E.nth ⟨j, hj⟩ = T.E.component (pos T hj)
definitionally).
The centre. Z_{-1} pulls back along ANY smooth h (Zminus1_pullback), stalkwise
(ext_stalkIdeal): at a point of Z_{-1}(T') both stalks are the stalk of the divisor
(stalkIdeal_Zminus1_eq of Center.lean, whose components are disjoint), elsewhere both are the
unit ideal. The two membership transports: a generic point of a component of h^{-1}(E^j) lies
over a generic point of E^j (mem_genericPoints_support_of_flat,
Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean) with the same order (ord_comap_of_smooth,
Hironaka/Scheme/IdealSheaf/Order/Smooth.lean); conversely a point over Z_{-1}(T) lifts its
generalisation along the flat h (Flat.generalizingMap), lies on a component of h^{-1}(E^j)
whose generic point maps to a generic point of E^j specialising to the selected one, hence equal
to it by the maximality clause of genericPoints. Then Z_{-1}|_S pulls back along any g : E'^j ⟶ E^j over h (centerS_pullback).
The restricted pair. The induced restriction restrictionMap : E'^j ⟶ E^j is Mathlib's
subschemeMap after the identification E'^j = h^{-1}(E^j) (component_eq_comap_component); it
lies over h, is smooth (a base change of h, AlgebraicGeometry.isPullback_subschemeι_comap) and
surjective when
h is. The induced morphism of the blown-up hypersurfaces restrictedMap is blowUpMap along it,
after the identification of the centres (centerS_comap_restrictionMap); it lies over h
(restrictedMap_comp_π, blowUpMap_π, AlgebraicGeometry.eqToHom_comp_blowUpπ), is smooth and
surjective when h is,
and the two restricted marked triples form a pull-back pair along it
(isPullbackOf_restrictedTriple): the ideals by markedTransform_comap_blowUpMap_of_pow_dvd (the
divisibility
hypothesis is trivial, the exceptional divisor of Z_{-1}|_S being the unit ideal,
exceptionalDivisor_centerS_eq_top of Composite.lean), the families by
totalTransform_comap_of_flat and the congruence of erase, both transported through the
eqToHom of the centres (markedTransform_comap_eqToHom, totalTransform_comap_eqToHom).
The output. rawSeq is the push-forward of cons (Z_{-1}|_S) (B(…)) along E^j ↪ X;
pullback_pushforward_of_isPullback (Hironaka/Scheme/BlowUpSequence/Pushforward.lean, with the
cartesian square of the restriction, isPullback_restrictionMap) turns h^*(rawSeq T) into the
push-forward of the pulled-back cons, whose centre is Z_{-1}(T')|_{S'} and whose tail is B's
value on the pulled-back restricted triple by B's own clause
(cons_pullback_restrictionMap_of_eq, cons_congr with the eqToHom transport
pullback_eqToHom_heq): rawSeq_pullback_of_surjective. For an arbitrary smooth h the tail
agrees only after deleting empty blow-ups (the second bullet of [Kol07, 34.1]); eraseEmpty passes
the push-forward and the cons (eraseEmpty_pushforward, eraseEmpty_cons_eraseEmpty,
Hironaka/Scheme/BlowUpSequence/EraseEmptyTransport.lean): eraseEmpty_rawSeq_pullback.
The functor. functor = rawSeq with its empty blow-ups deleted; by commutesWithSmooth_iff
(Hironaka/Scheme/BlowUpSequence/Functoriality.lean) only the second bullet is to be shown, and it
is eraseEmpty_rawSeq_pullback after eraseEmpty_pullback_eraseEmpty'; the first bullet alone is
rawSeq_pullback_of_surjective with eraseEmpty_pullback_of_flat_surjective
(functor_commutesWithSmooth, functor_commutesWithSmoothSurjections). The class transports
(isDBalanced_comap_of_smooth, domain_pullback_of_surjective) are [Kol07, Definition 83] under
the derivative's compatibility with smooth pull-back and the maxOrd lemmas of
Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean.
Used by FunctorialityBaseChange.lean, Assembly.lean and AssemblyZero.lean, and outside this
directory by Hironaka/Resolution/Algebraic/Kol07/Thm35/Principalization/Monomial.lean and
Hironaka/Resolution/Algebraic/OrderReduction/Step21Functorial.lean.
nth along an equality of families.
The j-th member of the pulled-back family is the inverse image of the j-th member (Kollár's
E^j_Y := h^{-1}(E^j), the proof of [Kol07, Lemma 102]).
Positions and the induced restriction #
The component at position j, as an index (reducible:
T.E.nth ⟨j, hj⟩ = T.E.component (pos T hj) definitionally).
Equations
- Hironaka.BD.pos T hj = (monoEquivOfFin T.E.ι ⋯) ⟨j, hj⟩
Instances For
The same, in the component form of the positions.
Surjective morphisms of schemes compose.
Transport of a marked transform along an equality of centres.
Transport of a total transform along an equality of centres.
erase at a position, along an equality of families.
The restriction of h to the j-th members: E'^j ⟶ E^j over h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restriction lies over h (Mathlib's subschemeMap_subschemeι).
The restriction is smooth: the base change of h along E^j ↪ X.
The restriction is surjective when h is (base change).
The square of the induced restriction over h is cartesian (transport of the canonical one).
Direction 1: a point of Z_{-1}(T') lies over a point of Z_{-1}(T).
Direction 2: a point over Z_{-1}(T) lies in Z_{-1}(T').
Z_{-1} pulls back along any smooth h.
Z_{-1}|_S pulls back along any g : E'^j ⟶ E^j over h.
Z_{-1}|_S pulls back along the induced restriction.
The induced morphism of the blown-up hypersurfaces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The induced morphism lies over the restriction (blowUpMap_π).
An eqToHom is smooth.
The induced morphism is smooth (blowUpMap along a smooth morphism).
The induced morphism is surjective when h is.
The divisibility hypothesis of markedTransform_comap_blowUpMap_of_pow_dvd for Z_{-1}|_S: its
exceptional
divisor is the unit ideal (exceptionalDivisor_centerS_eq_top).
The restricted marked triples form a pull-back pair along the induced morphism.
The restricted marked triples form a pull-back pair along a smooth morphism over h,
surjective when h is (existential form of isPullbackOf_restrictedTriple).
The output's first step and tail, pulled back along the induced restriction: the cons of the
pulled-back centre and the pulled-back tail (definitional), rewritten as the cons of
Z_{-1}(T')|_S' and the tail on the restricted triple of T' when B commutes with the induced
morphism.
The output sequence pulls back along a smooth surjection (the first bullet of [Kol07, 34.1]).
After deleting the empty blow-ups the outputs agree for any smooth h (the second bullet of
[Kol07, 34.1]).
Class transport and the functor level #
D-balancedness ([Kol07, Definition 83]) pulls back along a smooth morphism.
The pull-back of a triple of the standing class of [Kol07, Lemma 102] along a smooth surjection,
when of dimension ≤ n, is in the class.
BD_{n,m,j} commutes with smooth morphisms when B does ([Kol07, 34.1]; clause (2) of
[Kol07, Lemma 102]).
BD_{n,m,j} commutes with smooth surjections when B does.