Functoriality of BD_{n,m,j} under change of fields #
Clause (2) of [Kol07, Lemma 102], the change-of-fields part, which Kollár settles in one sentence:
"change of the base field commutes with restrictions". This module proves it for the construction
of Restriction.lean and Output.lean, for a general base-change square T'.IsBaseChangeOf T σ p
(Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean: a cartesian square over Spec σ,
I' = p^*I, E' = p^{-1}E; [Kol07, 34.2]), following the smooth case of
FunctorialityPullback.lean line by line with the flat p in place of the smooth h.
Orders under a change of fields. No pointwise comparison of orders along p is available for a
transcendental extension; what is needed is only the order at a GENERIC POINT of a member of E',
where it equals the order at its image (ord_comap_eq_of_mem_genericPoints_baseChange): the
member is a smooth divisor on both sides (smooth_component of Restriction.lean,
smooth_subschemeι_comap_comp_of_isPullback), so its stalk ideal at a generic point is the maximal
ideal on both sides and ord_comap_of_flat_of_stalkIdeal_eq
(Hironaka/Scheme/BlowUpSequence/BaseChangeOrder.lean) applies. With this the two membership
transports for Z_{-1} are as in the smooth case (flatness lifts generalisations, generic points of
components map to generic points, the maximality clause of genericPoints identifies the image):
Zminus1_baseChange, centerS_baseChange.
The restricted pair. The restriction restrictionMap of p to the j-th members and the induced
morphism restrictedMapBaseChange of the blown-up hypersurfaces are the smooth module's
constructions (they use only E' = p^{-1}E); the restriction is flat as a base change of p. The
two restricted marked triples form a BASE-CHANGE pair: the cartesian square over Spec σ is the
vertical paste of the blow-up square (isPullback_blowUpMap), the restriction square
(isPullback_restrictionMap) and the triples' square, transported to the identified centres
(isPullback_restrictedMapBaseChange); the ideal and family clauses are the flat transports
markedTransform_comap_blowUpMap_of_pow_dvd, totalTransform_comap_of_flat through the eqToHom
of the centres
(isBaseChangeOf_restrictedTriple).
The output and the functor. rawSeq transports by the flat form
pullback_pushforward_of_isPullback_of_flat (Hironaka/Scheme/BlowUpSequence/Pushforward.lean) and
B's own clause on the restricted pair, an EXACT equality (34.2 deletes no blow-ups):
rawSeq_baseChange. The functor's values differ from the outputs by eraseEmpty, which commutes
with the pull-back along the flat SURJECTION p (IsBaseChangeOf.surjective,
eraseEmpty_pullback_of_flat_surjective): functor_commutesWithBaseChange. The class transports
are [Kol07, Definition 83] under the derivative's compatibility with the base-change square
(isDBalanced_comap_of_isPullback_specMap) and maxOrd_comap_of_isPullback_specMap
(Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean) with the base-change stability of
the relative dimension (domain_baseChange).
Used by AssemblyZero.lean.
Along a change of fields, the order at a generic point of the j-th member of T' is the order
at its image, a generic point of the j-th member of T.
Direction 1 (base change): a point of Z_{-1}(T') lies over a point of Z_{-1}(T).
Direction 2 (base change): a point over Z_{-1}(T) lies in Z_{-1}(T').
Z_{-1} is compatible with a change of fields.
Z_{-1}|_S is compatible with a change of fields along any g over p.
Z_{-1}|_S is compatible with the induced restriction of p.
The induced morphism of the blown-up hypersurfaces along a change of fields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The induced morphism lies over the restriction of p (blowUpMap_π).
The restriction of p is flat (a base change of the flat p).
The base-change square of the blown-up hypersurfaces over Spec σ, by pasting the blow-up
square, the restriction square and the base-change square of the triples.
The restricted marked triples form a base-change pair along the induced morphism.
The restricted marked triples form a base-change pair along the morphism of the blown-up
hypersurfaces induced by p (existential form of isBaseChangeOf_restrictedTriple).
The output sequence of the base change is the pull-back of the output sequence.
D-balancedness ([Kol07, Definition 83]) is preserved by a change of fields.
The base change of a triple of the standing class of [Kol07, Lemma 102] stays in the class.
BD_{n,m,j} commutes with change of fields when B, B' do ([Kol07, 34.2]; clause (2) of
[Kol07, Lemma 102]).