Regular systems of parameters along a smooth stalk map #
Pulling back a smooth blow-up sequence along a smooth morphism h : Y ⟶ X (Kol07, 30.1 and
34.1; [Wlo05, Proposition 2.4.2]) transports the simple normal crossing conditions of
[Kol07, Definition 24] along h: a regular system of parameters z_1, …, z_n of 𝒪_{X, h y} in
which the components of E through h y are coordinate hypersurfaces must extend, through the
stalk map φ : 𝒪_{X, h y} → 𝒪_{Y, y}, to a regular system of parameters of 𝒪_{Y, y}. This
module proves that local statement (exists_isRegularSystemOfParameters_stalkMap); the normal
crossing predicates themselves are transported in Hironaka/Scheme/BlowUpSequence/PullbackSnc.lean.
The argument #
Both stalks are regular local rings (the schemes are smooth over k), and φ is a formally
smooth local homomorphism (Scheme.Hom.formallySmooth_stalkMap in
Hironaka/Scheme/IdealSheaf/Derivative/Pullback.lean: every point lies in Mathlib's smooth locus).
The classes of z_1, …, z_n form a basis of 𝔪_A/𝔪_A²; because κ(A)/k is separable (k perfect)
the conormal map 𝔪_A/𝔪_A² → κ(A) ⊗_A Ω_{A/k} is injective (injective_cotangentSpaceToTensor), so
there are k-derivations δ_i : A → κ(A) with δ_i z_j = δ_ij. Pushed into κ(B) and extended
along the formally smooth φ (exists_derivation_extend, the Jacobi–Zariski sequence with
H¹(L_{B/A}) = 0 and Ω_{B/A} projective), they give derivations ∂_i : B → κ(B) with
∂_i (φ z_j) = δ_ij, which detect the linear independence of the classes of the φ z_j in
𝔪_B/𝔪_B² (linearIndependent_toCotangent_of_derivations_residueField). A linearly independent
family in 𝔪_B/𝔪_B² extends to a regular system of parameters of B
(exists_span_eq_maximalIdeal_of_linearIndependent, [TSPA, Tag 00NR]), which completes the proof.
The facts about formally smooth algebras used here are standard ([TSPA, Tags 00TA, 00TI and 00TV]); none of the lemmas of this module is stated in the printed proofs.
Extension of derivations along a formally smooth map #
Along a formally smooth A → B every k-derivation of A into a B-module extends to B
(the infinitesimal lifting property in its Kähler form, [TSPA, Tag 00TI]). The Jacobi–Zariski
sequence H¹(L_{B/A}) → B ⊗_A Ω_{A/k} → Ω_{B/k} → Ω_{B/A} → 0 has H¹ = 0 and Ω_{B/A}
projective (Mathlib's definition of formal smoothness), so B ⊗_A Ω_{A/k} → Ω_{B/k} is a split
injection and a linear functional on it extends.
Independence in the cotangent space detected by derivations into the residue field #
The maximal ideal acts trivially on the residue field.
A derivation into the residue field kills 𝔪² (Leibniz).
The independence criterion linearIndependent_toCotangent_of_derivations with derivations
into the residue field: if D_i (w_j) = δ_ij in κ then the classes of the w_j in 𝔪/𝔪² are
linearly independent.
The algebraic core: parameters extend along a formally smooth local homomorphism #
For a formally smooth local homomorphism A → B of regular local rings with κ(A)/k
separable, the image of a regular system of parameters of A is part of a regular system of
parameters of B; the algebra behind the proof of [Wlo05, Proposition 2.4.2] ("C'_i has simple
normal crossings with E'_i"). The classes of z_1, …, z_n form a basis of 𝔪_A/𝔪_A²; the
conormal map 𝔪_A/𝔪_A² → κ(A) ⊗ Ω_{A/k} is injective, so dual derivations δ_i : A → κ(A) with
δ_i z_j = δ_ij exist; pushed to κ(B) and extended along A → B (exists_derivation_extend)
they detect the independence of the classes of the φ(z_j) in 𝔪_B/𝔪_B², and a linearly
independent family in 𝔪_B/𝔪_B² extends to a regular system of parameters of B.
At the stalks of a smooth morphism #
The stalk of a scheme locally of finite type over k is essentially of finite type over k:
Γ(U) is of finite type for an affine U ∋ x, and the stalk is its localization.
Along the stalk map of a smooth morphism between schemes smooth over a perfect field, a regular
system of parameters at h y extends to one at y: the local statement behind the transport of
simple normal crossings [Kol07, Definition 24] along a smooth morphism
([Wlo05, Proposition 2.4.2, proof]).