The derivative ideal under a change of the base field #
[Kol07, Lemma 74 (4)] says that the derivative ideal commutes with smooth pull-back
(Hironaka/Scheme/IdealSheaf/Derivative/Pullback.lean). Kollár also asks that resolution commute
with a change of fields σ : k → L ([Kol07, 34.2]: the fibre product X_L = X ×_{Spec k} Spec L,
with I_L and E_L), and the functoriality of order reduction under such a change needs the
derivative ideals, and with them the tuning ideal, to commute with it. This module proves that fact:
for k of characteristic zero and X smooth over k, on a cartesian square
sq : IsPullback p g' f (Spec.map σ) with p : X_L → X the projection and g' : X_L → Spec L the
base-changed structure morphism,
D_L(p^* I) = p^* D_k(I), hence D_L^r(p^* I) = p^* D_k^r(I)
(derivative_comap_of_isPullback_specMap, derivativeIter_comap_of_isPullback_specMap), where
D_L is the derivative ideal of the L-scheme X_L and D_k that of the k-scheme X. The
statement is not in the sources; Włodarczyk's [Wlo05, Lemma 2.9.3] is the analogous compatibility
of the homogenized ideal with smooth morphisms.
The argument #
Both inclusions are checked on stalks (ext_stalkIdeal), through stalkIdeal_derivative and
stalkIdeal_comap: at y ∈ X_L with x = p y, A = 𝒪_{X, x} is a k-algebra, B = 𝒪_{X_L, y}
an L-algebra, and φ : A → B the stalk map; to show: D_L(J B) = D_k(J) B for J = I_x.
D_L(J B) ⊆ D_k(J) B: anL-derivation ofBis ak-derivation (Derivation.restrictScalars, the towerk → L → Bcoming from the commutativity of the square), soD_L(J B) ⊆ D_k(J B), andD_k(J B) = D_k(J) BisIdeal.derivative_map_of_formallySmoothofHironaka/Algebra/Derivative/Extension.lean:φis formally smooth (formallySmooth_stalkMap_of_isPullback_specMap,Hironaka/Scheme/BlowUpSequence/BaseChangeParameters.lean, where[CharZero k]enters) andΩ_{A/k}is finite projective (Xsmooth overk).D_k(J) B ⊆ D_L(J B): it suffices that everyk-derivationδofAlifts to anL-derivationδ'ofBwithδ' ∘ φ = φ ∘ δ, for thenφ(δ f) = δ'(φ f) ∈ D_L(J B). Such lifts exist for a base changeB = L ⊗_k A(Mathlib'sAlgebra.IsPushout k L A B): the canonical isomorphismB ⊗_A Ω_{A/k} ≅ Ω_{B/L}(KaehlerDifferential.tensorKaehlerEquiv) turns theA-linear mapΩ_{A/k} → B,da ↦ φ(δ a), into aB-linear mapΩ_{B/L} → B, that is, anL-derivation ofB(Derivation.exists_extension_of_isPushout). The stalks are not a pushout, so this inclusion is proved on sections: for an affineU ∋ x,p⁻¹U = U ×_{Spec k} Spec Lis affine andΓ(p⁻¹U) = L ⊗_k Γ(U), by Mathlib'sisPushout_appTop_of_isPullbackfor the restricted square, transported toΓ(X, U) → Γ(X_L, p⁻¹U)along theΓSpecIsoandtopIsoisomorphisms and read asAlgebra.IsPushoutbyCommRingCat.isPushout_iff_isPushout(isPushout_appLE_of_isPullback_specMap). The section-level inclusionD_k(I(U)) Γ(p⁻¹U) ⊆ D_L(I(U) Γ(p⁻¹U))then passes to the stalk throughstalkIdeal_eq_map_germ,ideal_comap_of_le(Hironaka/Scheme/BlowUp/InverseImage.lean) andideal_derivative(Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean).
Used for the functoriality of order reduction under a change of fields
(Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean,
Hironaka/Resolution/Algebraic/OrderReduction/Step3Clauses.lean,
Hironaka/Resolution/Algebraic/MarkedOrderReduction/BaseChangeParameters.lean,
Hironaka/Resolution/Algebraic/Tuning/Pullback.lean,
Hironaka/Resolution/Algebraic/BoundaryClearing/FunctorialityBaseChange.lean).
Algebra: derivations along a base change #
For B = L ⊗_k A a base change of the k-algebra A along k → L, every k-derivation δ
of A lifts to an L-derivation δ' of B with δ' ∘ φ = φ ∘ δ: under
Ω_{B/L} ≅ B ⊗_A Ω_{A/k} (KaehlerDifferential.tensorKaehlerEquiv), δ' is the B-linear map
b ⊗ da ↦ b φ(δ a).
D_k(J) B ⊆ D_L(J B) for B = L ⊗_k A: the L-derivation lifts of
Derivation.exists_extension_of_isPushout carry φ(δ f) = δ'(φ f) into D_L(J B) (the argument
of map_derivative_le_of_forall_exists_extension in Hironaka/Algebra/Derivative/Extension.lean,
with L-derivations of B).
D_L(J B) ⊆ D_k(J) B for a tower k → L → B, k → A → B with B formally smooth over A
and Ω_{A/k} finite projective: an L-derivation of B is a k-derivation, so
D_L(J B) ⊆ D_k(J B), and D_k(J B) = D_k(J) B is derivative_map_of_formallySmooth.
Geometry: the algebra structures of a base-change square #
The k-algebra structure of Γ(Y, V) induced by g' ≫ Spec σ is the L-algebra structure
induced by g' restricted along σ: the tower k → L → Γ(Y, V).
The stalk form of algebraMap_sectionsAlgebra_comp_specMap: the tower k → L → 𝒪_{Y, y}.
The scalar tower k → Γ(X, U) → Γ(Y, V) for the structures induced by fX, f ≫ fX and the
map on sections f.appLE U V e (the sections form of isScalarTower_stalkAlgebra_stalkMap in
Hironaka/Scheme/IdealSheaf/Derivative/Pullback.lean).
Global sections of the open subscheme V, followed by topIso, are the sections over V:
Γ(V.ι ≫ g) ≫ V.topIso.hom = g.appLE ⊤ V.
The restriction p ∣_ U on global sections, read through the topIso identifications, is
p.appLE U (p⁻¹U).
On the base-change square, the k-algebra structure of Γ(Y, V) induced by p ≫ f is the
L-structure induced by g' restricted along σ (p ≫ f = g' ≫ Spec σ).
The stalk form of algebraMap_sectionsAlgebra_of_isPullback_specMap.
Over an affine open U ⊆ X, the sections of the base change X_L → X of [Kol07, 34.2] form a
pushout of rings, Γ(X_L, p⁻¹U) = L ⊗_k Γ(X, U): Mathlib's isPushout_appTop_of_isPullback for
the restricted square p⁻¹U = U ×_{Spec k} Spec L, transported along the ΓSpecIso and topIso
identifications of its corners.
The derivative ideal commutes with a change of the base field ([Kol07, Lemma 74 (4)] for
the base change of [Kol07, 34.2]): on the base-change square p : X_L → X along σ : k → L with
k of characteristic zero and X smooth over k, D_L(p^* I) = p^* D_k(I). Stalkwise:
D_L(J B) ⊆ D_k(J) B since L-derivations are k-derivations and the stalk map is formally
smooth; D_k(J) B ⊆ D_L(J B) on the sections over an affine U ∋ p y, where
Γ(p⁻¹U) = L ⊗_k Γ(U) lifts k-derivations to L-derivations.
The iterates: D_L^r(p^* I) = p^* D_k^r(I) along a change of fields.