Clauses (1)–(2) of order reduction for the globalised functor #
Step 3 of the proof of [Kol07, Theorem 103] defines BO_{n,m} by descent from a cover and
asserts the clauses of the theorem for it through the locality of the functoriality package
([Kol07, 34]: "the claimed isomorphism is unique, and hence the existence is a local question").
The argument here is one pattern, used four times: a local cover g : TU → T (hypothesis (2)(i) of
[Kol07, Theorem 105], exists_isLocalCover) is pulled back to the source of the morphism under
study (Hironaka/Resolution/Algebraic/OrderReduction/Step3Cover.lean, or its base-change form
exists_localCover_baseChange below); both sides of the desired identity pull back along the
surjective open-immersion coproduct g' to the local functor's value on the pulled-back cover,
by the descent identity globalize_seq_pullback on one side and by the same identity followed by
the corresponding theorem for maxContactCase on the other; and a pull-back along a surjective
flat morphism is injective on blow-up sequences (pullback_injective_of_surjective). The empty
triple is the degenerate case, where every value is nil.
- Clause (1),
functor_maxOrd_lt: the maximal order at the last stage is read off the cover. The last-stage lift is surjective (surjective_pullbackStageHom), the weak transform of the pull-back is the pull-back of the weak transform (IsOrderSeq.weakTransformSeq_pullback), the maximal order does not decrease under a surjective pull-back (maxOrd_le_maxOrd_comap_of_surjective), and on the cover it ismaxOrd_maxContactCase_lt. - The first clause of [Kol07, 34.1],
functor_commutesWithSmoothSurjections: on the pulled-back cover the local functor commutes with the smooth surjection (hypothesis (3) of Theorem 105). - The second clause of [Kol07, 34.1],
functor_commutesWithSmooth: the deletion of empty blow-ups moves through the pull-back along the surjective flatg'(eraseEmpty_pullback_of_flat_surjective), and on the pieces the identity ismaxContactCase_eraseEmpty_pullback, under the indifferencehindof the boundary-clearing data to empty boundary members. - [Kol07, 34.2],
functor_commutesWithBaseChange: the cover pulled back along the base-change projection is a base-change pair of local triples (exists_localCover_baseChange, with the transports of a smooth hypersurface of maximal contact along the base-change square,isSmoothDivisor_comap_of_isPullback_specMapandisMaximalContact_comap_of_isPullback_specMap), and on the pieces the identity ismaxContactCase_baseChange.
The clauses are packaged as BOData n m in
Hironaka/Resolution/Algebraic/OrderReduction/Step3Data.lean.
The inverse image of a hypersurface of maximal contact under the projection of a base-change
square over a field extension is one for the pulled-back ideal ([Kol07, 34.2]): MC is D^{m-1}
and the derivative commutes with the square (derivativeIter_comap_of_isPullback_specMap).
The inverse image of a smooth divisor under the projection of a base-change square over a field
extension is a smooth divisor ([Kol07, 34.2]; isSnc_comap_of_isPullback_specMap on the one-member
family, as isSmoothDivisor_comap_of_smooth for smooth morphisms).
The pull-back of a local cover along a base-change projection ([Kol07, 34.2], with the fibre
product of the proof of [Kol07, Theorem 105]): for a local cover g : TU → T and a base-change
pair T'.IsBaseChangeOf T σ p, the fibre product W = TU ×_T T' is a local cover of T' along
the second projection and carries the base-change data of TU along the first (the two squares
paste to a square over Spec σ); W lies in the local class by boClass_isPullbackOf on the open
leg and the two transports above along the base-change leg.
The descent identity of Step 3 of the proof of [Kol07, Theorem 103] along a local cover:
g^* BO_{n,m}(X, I, E) = BO_{n,m}(X^*, g^* I, g^{-1} E) (globalize_seq_pullback).
On an empty scheme every ideal sheaf has maximal order 0.
Clause (1) of [Kol07, Theorem 103] for BO_{n,m}: max-ord I_r < m, read off a local cover
through the surjective last-stage lift; the clause is local on X_r.
Clause (2) of [Kol07, Theorem 103] for BO_{n,m}, the first clause of [Kol07, 34.1]:
BO_{n,m} commutes with smooth surjections. Both sides pull back along the pulled-back cover to
the local functor's value on the pulled-back local triple (hypothesis (3) of
[Kol07, Theorem 105]), and a surjective flat pull-back is injective on sequences.
Clause (2) of [Kol07, Theorem 103] for BO_{n,m}, both clauses of [Kol07, 34.1]: BO_{n,m}
commutes with smooth morphisms. The second clause (an arbitrary smooth h, empty blow-ups
deleted) holds under the indifference hind of the boundary-clearing data to empty boundary
members: the deletion moves through the pull-back along the surjective flat g', and on the pieces
the identity is maxContactCase_eraseEmpty_pullback.
Clause (2) of [Kol07, Theorem 103] for BO_{n,m}, [Kol07, 34.2]: BO_{n,m} commutes with
change of fields. The cover is pulled back along the base-change projection
(exists_localCover_baseChange), the identity on the pieces is maxContactCase_baseChange, and
the pull-back along the surjective open-immersion coproduct is injective.