Regular systems of parameters and simple normal crossings 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 σ, a regular system of parameters of 𝒪_{X, p y} extends along the
stalk map to one of 𝒪_{X_{L,σ}, y}, so the simple normal crossing conditions IsSncAt, IsSnc
and HasSncWith of [Kol07, Definition 24] transport along p. These are the analogues, for the
change of fields of [Kol07, 34.2], of exists_isSncAt_comap_of_smooth, isSnc_comap_of_smooth
and hasSncWith_comap_of_smooth for a smooth morphism
(Hironaka/Scheme/BlowUpSequence/PullbackSnc.lean), whose proofs are followed step by step. None of
this is in the sources.
The argument #
The algebraic core exists_isRegularSystemOfParameters_extend asks of the local homomorphism
A = 𝒪_{X, p y} → B = 𝒪_{X_{L,σ}, y} only that both rings be regular (the schemes are smooth over
their fields), that it be local and formally smooth, and that κ(A)/k be formally smooth
(k perfect, κ(A) essentially of finite type). The one new fact is the formal smoothness of the
base-change stalk map:
- every field extension of a field of characteristic zero is formally smooth
(
Algebra.FormallySmooth.of_charZero): choose a transcendence basis (exists_isTranscendenceBasis');Lis algebraic, hence separable in characteristic zero (Algebra.IsSeparable.of_integral), over the purely transcendental intermediate field, andAlgebra.FormallySmooth.of_algebraicIndependent_of_isSeparableconcludes (the easy direction of [TSPA, Tag 031X]; no finiteness needed); - over an affine
U ∋ p ythe morphismprestricts to the affinep⁻¹U = U ×_{Spec k} Spec L(pis an affine morphism, the base change ofSpec σ; the restricted square is the restriction square ofppasted on the base-change square), andRingHom.FormallySmoothis stable under base change (IsStableUnderBaseChange.pullback_fst_appTop), soΓ(U) → Γ(p⁻¹U)is formally smooth; - localizing (
Algebra.FormallySmooth.of_isLocalization,comp) givesIsSmoothAt Γ(U) qat the prime ofy, whichformallySmooth_stalkMap_iffturns into the formal smoothness of the stalk map ofp ∣_ U, hence ofp(morphismRestrictStalkMap).
Every field extension in characteristic zero is formally smooth #
A field extension L/k with k of characteristic zero is formally smooth (the easy direction
of [TSPA, Tag 031X]): L is separable (Algebra.IsSeparable.of_integral) over the purely
transcendental extension generated by a transcendence basis, and separably generated extensions
are formally smooth (Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable). No
finiteness is assumed.
The morphism Spec σ is formally smooth on global sections when k has characteristic zero
(Algebra.FormallySmooth.of_charZero, read through ΓSpecIso).
The restriction of p over an affine open U ⊆ X is formally smooth on global sections:
p⁻¹U = U ×_{Spec k} Spec L and formal smoothness is stable under base change
(IsStableUnderBaseChange.pullback_fst_appTop).
The stalk map of the projection of a base-change square along a field extension in
characteristic zero is formally smooth: formallySmooth_stalkMap_iff on the affine restriction
p ∣_ U : p⁻¹U → U with Γ(U) → Γ(p⁻¹U) formally smooth and the localization at the prime of y
(IsSmoothAt), transported to p by morphismRestrictStalkMap.
The local statement: along the stalk map of the projection of a base-change square along a
field extension in characteristic zero, a regular system of parameters at p y extends to one at
y (exists_isRegularSystemOfParameters_extend with the formal smoothness of the stalk map from
formallySmooth_stalkMap_of_isPullback_specMap).
Simple normal crossings under a field extension #
The pointwise statement: the simple normal crossing data of E at p y
([Kol07, Definition 24]) transport to simple normal crossing data of p⁻¹ E at y (the analogue
of exists_isSncAt_comap_of_smooth for the base change).
A simple normal crossing family on X smooth over k pulls back to one on X_{L,σ} (Kollár's
E_{L,σ}, [Kol07, 34.2]; the analogue of isSnc_comap_of_smooth for the base change): the
components' subschemes are regular because their stalks are quotients of the regular local rings
of X_{L,σ} by a member of a regular system of parameters.
Simple normal crossings of a closed subscheme with a family (Kol07, Definition 24, condition
(4)) are preserved by the base change along a field extension (the analogue of
hasSncWith_comap_of_smooth).