From the stalk of a smooth scheme to Kollár's K⟦x⟧ computations #
The ring-level results of Hironaka/Algebra/Local/CohenDerivation.lean ([Kol07, Proposition 94] on
the chart) are stated for a regular local k-algebra R with coordinates c whose derivations are
k-linear and whose residue field is algebraic over k, and for the Cohen isomorphism
cohenAlgEquivCoords c σ hσ built from c. At a closed point p of a smooth k-scheme this file
supplies the inputs and translates the outputs into the form used by the proof of the formal half
of Theorem 92 (Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivExists.lean):
isAlgebraic_residueField_of_isClosed: at a closed pointκ(p)is algebraic overk(trdeg_k κ(p) = 0,trdeg_residueField_stalk_eq_zero_of_isClosed).exists_regularCoords_eq: coordinates on𝒪_{X,p}with a prescribed regular system of parameterszasc.x,k-linear and spanning thek-derivations: the coordinates ofexists_regularCoords_stalk_of_isAlgebraicchanged tozbychangeCoords, withtransportPderiv_isLinearOver,transport_overandtransportPderiv_comm_over.isMCInvariant_stalk: MC-invariance of the ideal sheafIin the sense of [Kol07, 53.1] givesMC(I_p)·D(I_p) ⊆ I_pin any such coordinates (stalkIdeal_mul,stalkIdeal_MC,stalkIdeal_derivativeandderivative_eq_D), hence, since derivatives commute with completion ([Kol07, Lemma 74 (5)]), forÎin the completed coordinates (isMCInvariant_adicCompletion).completionIdeal_MC_le_maximalIdeal:\widehat{MC(I)} ⊆ 𝔪Ô_{X,p}at a point ofcosupp(I, m)(MC(I)has order1there, [Kol07, Definition 79]).cohenAlgEquiv_eq: ak-algebra isomorphismΦ : κ(p)⟦X⟧ ≃ₐ[k] Ô_{X,p}withΦ(Xᵢ) = ι(c.xᵢ)whose constants are a coefficient field is the Cohen isomorphismcohenAlgEquivCoords c σ hσforσ := Φ ∘ C:Φ'⁻¹ ∘ Φis aK-algebra automorphism ofK⟦X⟧fixing theXᵢ, hence the identity (algHom_ext_of_forall_X_mem; this is the identificationÔ_{p,X} ≅ K⟦x₁, …, xₙ⟧of [Kol07, Notation 93]). So the statements ofFormalEquivExists.lean, quantified over any suchΦ, follow from the ring-level results for the Cohen isomorphism:isInvariantOnePlus_comap_completionIdeal([Kol07, Proposition 94 (1)]) andmap_comap_completionIdeal_eq_of_isOnePlus(the equalityφ^* Î = Î).
At a closed point the residue field is algebraic over k (trdeg_k κ(p) = 0).
Coordinates on the stalk at a closed point that are k-linear and span the k-derivations,
with a prescribed regular system of parameters z as the coordinates: change of coordinates
(changeCoords) from any such structure.
[Kol07, 53.1] at the stalk: if I is MC-invariant then MC(I_p)·D(I_p) ⊆ I_p in coordinates
c that are k-linear and span the k-derivations (the predicate
RegularCoords.IsMCInvariant).
MC-invariance passes to the completion, since derivatives commute with completion
([Kol07, Lemma 74 (5)]): Î is MC-invariant in the completed coordinates.
At a point of cosupp(I, m) the completed maximal contact ideal lies in the maximal ideal of
Ô_{X,p} (MC(I) has order 1 there, the remark in [Kol07, Definition 79]).
The coefficient field Φ ∘ C of a k-algebra isomorphism Φ : κ(p)⟦X⟧ ≃ₐ[k] Ô_{X,p}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coefficient field of Φ unfolded: (Φ ∘ C)(a) = Φ(C a).
The identification Ô_{p,X} ≅ K⟦x₁, …, xₙ⟧ of [Kol07, Notation 93] as a uniqueness statement:
a k-algebra isomorphism Φ : κ(p)⟦X⟧ ≃ₐ[k] Ô_{X,p} with Φ(Xᵢ) = ι(c.xᵢ) whose constants form
a coefficient field is the Cohen isomorphism of the coordinates c for the coefficient field
Φ ∘ C.