The order along a center under a field extension #
For σ : k →+* L a field extension in characteristic zero and p : X_{L,σ} → X the projection of
a cartesian square over Spec σ (flat, but not smooth or of finite type when L/k is infinite),
the order of an ideal at a generic point η' of a component of the base-changed center
(Z)_{L,σ} equals its order at η = p η', provided the center is smooth over k, as the centers
of a smooth blow-up sequence are ([Kol07, Notation 19]; IsSmooth). Kollár asserts that the
change of fields "will hold automatically for all blow-up sequence functors that we construct"
[Kol07, 34.2]; this module and its two sibling modules supply the transports.
The argument #
At a generic point η of the support of a center Z with V(Z) → Spec k smooth, the stalk
ideal is the maximal ideal: 𝒪_{X,η}/Z_η is regular, hence a domain, so Z_η is prime, and
exists_genericPoint_of_isPrime_stalkIdeal produces the generic point η₀ of the component
through η with Z_{η₀} = 𝔪_{η₀} and η₀ ⤳ η; η being itself a generic point of Z.support
(maximal for specialization), η₀ = η. The same holds at η' on X_{L,σ} because
V(Z.comap p) → Spec L is the base change of V(Z) → Spec k (the closed-subscheme square pasted
on the base-change square) and smoothness is stable under base change. Then
𝔪_η 𝒪_{η'} = (Z.comap p)_{η'} = 𝔪_{η'} (stalkIdeal_comap), the stalk map is flat
(Flat.stalkMap) and local, and ord_map_eq_of_flat_of_map_maximalIdeal_eq gives
ord_{η'}(p^* I) = ord_η I. No reducedness of the fibre κ(η) ⊗_k L is needed, because the
centers are smooth. The ≥ m form holds along every flat morphism (ord_le_ord_map).
With this, the weak transform of [Kol07, Definition 60] commutes with the base change exactly as
with a smooth pullback (weakTransform_comap_of_orderAlong_of_isPullback_specMap, by
weakTransform_eq_markedTransform_of_smooth on both sides and
markedTransform_comap_blowUpMap_of_pow_dvd),
and so do the induced ideals of a smooth blow-up sequence of order m along the base-changed
sequence (IsOrderSeq.weakTransformSeq_pullback_mk_of_isPullback_specMap, induction with the
stage squares of Hironaka/Scheme/BlowUpSequence/BaseChange.lean); the marked transforms commute
with every flat base change (IsOrderGeSeq.markedTransformSeq_pullback_mk_of_flat). None of this is
in the sources, which assert the transports without proof.
Generic points of smooth centers #
At a generic point η of the support of a center Z smooth over k (on X smooth over
k), the stalk ideal of Z is the maximal ideal: 𝒪_{X,η}/Z_η is regular, so Z_η is prime,
and the generic point of the component of V(Z) through η
(exists_genericPoint_of_isPrime_stalkIdeal) is η itself. Not in the sources.
The order at a point under a flat morphism with 𝔪_A B = 𝔪_B #
For a flat p and a point η' at which the stalk ideals of Z and of Z.comap p are the
maximal ideals, the order of every ideal sheaf is preserved, ord_{η'}(p^* I) = ord_{p η'} I
(ord_map_eq_of_flat_of_map_maximalIdeal_eq).
The base-changed center is smooth over the extended field #
The base change of a smooth closed subscheme along any cartesian square is smooth: the
closed-subscheme square AlgebraicGeometry.isPullback_subschemeι_comap pasted on the square (one
step of
Triple.IsBaseChangeOf.isSmooth_pullback).
The order along a center under a field extension #
The projection of a base-change square along a field extension is flat
(IsBaseChangeOf.flat for an arbitrary cartesian square).
The projection of a base-change square along a field extension is surjective
(IsBaseChangeOf.surjective for an arbitrary cartesian square; the base change of the surjective
Spec L → Spec k, flat_and_surjective_specMap).
The base change of a smooth k-scheme is a smooth L-scheme.
The base change of a k-scheme smooth of relative dimension n is smooth of relative
dimension n over L.
The order along a smooth center is preserved by base change along a field extension,
ord_{(Z)_{L,σ}}(p^* I) = ord_Z I (needed for the change of fields of [Kol07, 34.2]; not in the
sources): at a generic point η' of (Z)_{L,σ} both stalk ideals are the maximal ideals
(stalkIdeal_eq_maximalIdeal_of_mem_genericPoints on X and on X_{L,σ}), and the flat local
stalk map preserves the order (ord_comap_of_flat_of_stalkIdeal_eq).
The ≥ m form: orders never drop under a local homomorphism, so the condition "order ≥ m
along the center" transports along every flat morphism.
The weak transform under a field extension #
In the setting of [Kol07, Definition 66] the weak transform commutes with the base change
along a field extension (the analogue of weakTransform_comap_of_orderAlong for a smooth
pullback): both sides are the marked transform with mark m
(weakTransform_eq_markedTransform_of_smooth; the order along the base-changed center by
ordAlongEq_comap_of_isPullback_specMap, the center smooth over L by base change), and the
marked transform pulls back along the flat morphism of blow-ups
(markedTransform_comap_blowUpMap_of_pow_dvd).
The induced ideals of the base-changed sequence are the inverse images of the induced ideals
under the stage lifts, in the ⟨j, hj⟩ form (the analogue of
IsOrderSeq.weakTransformSeq_pullback_mk for a smooth pullback). Induction on the sequence; the
square of the next stage is the base-change square of the blow-up (isPullback_blowUpMap) pasted
on the given one.
The induced ideals of the base-changed sequence, for every stage.
The marked transforms along any flat base change #
The induced marked ideals of a smooth blow-up sequence of order ≥ m pull back along every
flat morphism, in the ⟨j, hj⟩ form (IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom_mk
for
a flat h): markedTransform_comap_blowUpMap_of_pow_dvd at each stage, the divisibility
F^m ∣ π^* I from
the order condition.
The induced marked ideals along a flat base change, for every stage.