Derivatives and MC-invariance across the Cohen isomorphism #
In the proof of the formal equivalence theorem [Kol07, 95], Kollár identifies Ô_{p,X} with
K⟦x₁, …, xₙ⟧ by the Cohen structure theorem ([Kol07, Definition 55]) so that Proposition 94
applies there: since x₁ − x₁' ∈ MC(I), the automorphism φ^* sending x₁' to x₁ is of the
form 1 + MC(I), and Proposition 94 gives φ^* Î = Î. Proposition 94 is proved on
K⟦X⟧ with its standard coordinates (Hironaka/Algebra/Local/Prop94.lean); MC-invariance of I
passes to the completion in the coordinates ĉ = c.adicCompletion
(Hironaka/Algebra/Local/DerivativeCompletion.lean, Kollár's D(Î) = D(I)^). This file carries
the derivative ideals from (R̂, ĉ) to
(K⟦X⟧, ∂/∂Xᵢ) along the k-linear Cohen isomorphism Φ of
Hironaka/Algebra/Local/CoefficientFieldOver.lean, and applies Proposition 94.
Why it holds. Let R be a regular local k-algebra with coordinates c whose ∂ᵢ are
k-linear, K = R/𝔪 algebraic over k (the residue field of a closed point), σ a k-linear
coefficient field and Φ : K⟦X⟧ ≃ₐ[k] R̂ the Cohen isomorphism with Φ(Xⱼ) = ι(xⱼ),
Φ(C a) = σ(a).
- The completed derivations kill the coefficient field
(
adicCompletion_pderiv_coefficientField):∂̂ᵢkillsι(k)(Hironaka/Algebra/Local/CompletionCoords.lean), so it is ak-derivation ofR̂; fora ∈ Kwith minimal polynomialPoverk,P(σ a) = 0, henceP'(σ a)·∂̂ᵢ(σ a) = 0, andP'(σ a) = σ(P'(a))is a unit becausePis separable (characteristic zero) andσis a field embedding. - Transport of the coordinate derivations (
cohenAlgEquivCoords_pderiv):Φ⁻¹ ∘ ∂̂ᵢ ∘ Φis aK-derivation ofK⟦X⟧(by 1), with valueδᵢⱼonXⱼ;mvPowerSeries_spansDerivationsofHironaka/Algebra/Local/CoordsOver.lean(aK-derivation ofK⟦X⟧is∑ⱼ δ(Xⱼ) ∂/∂Xⱼ) makes it∂/∂Xᵢ. SoΦ(∂F/∂Xᵢ) = ∂̂ᵢ(Φ F). - Transport of the derivative ideals (
D_map_cohenAlgEquivCoords,Dpow_map_cohenAlgEquivCoords,MC_map_cohenAlgEquivCoords):Φ(D(J)) = D(Φ(J))by 2 and the description ofDon generators (D_span); iterate. - MC-invariance transports (
isMCInvariant_comap_cohenAlgEquivCoords) and Proposition 94 applies (isInvariantOnePlus_comap_cohenAlgEquivCoords):Φ⁻¹(Î)is invariant under every automorphism of the form1 + Φ⁻¹(MC(Î)), the1 + MC(I)of Kollár's proof. - Equality from inclusion (
Ideal.map_eq_of_map_le,map_comap_cohenAlgEquivCoords_eq_of_isOnePlus): Proposition 94 givesg(J) ⊆ J(the primitive ofIsInvariantOnePlus); for an automorphismgof a Noetherian ring the chainJ ⊆ g⁻¹J ⊆ g⁻²J ⊆ ⋯stabilizes, whenceg(J) = J— Kollár'sφ^* Î = Î, [Kol07, Definition 91, (2)].
The maximal ideal of a local ring is the preimage of the maximal ideal under a ring isomorphism.
The completed coordinate derivations are k-linear (adicCompletion_algebraMap_eq_zero).
When the residue field is algebraic over k (the residue field of a closed point), the
completed coordinate derivations ∂̂ᵢ vanish on the k-linear coefficient field σ(K) — for
a ∈ K with minimal polynomial P, P'(σ a)·∂̂ᵢ(σ a) = 0 and P'(σ a) = σ(P'(a)) is a unit,
P being separable in characteristic zero.
The Cohen isomorphism of the coordinates c for the coefficient field σ.
Equations
- IsLocalRing.cohenAlgEquivCoords c σ hσ = IsLocalRing.cohenAlgEquivOver σ hσ c.x ⋯ ⋯
Instances For
The coordinate derivation ∂/∂Xᵢ of K⟦X⟧ corresponds under the Cohen isomorphism to the
completed coordinate derivation ∂̂ᵢ of R̂: Φ(∂F/∂Xᵢ) = ∂̂ᵢ(Φ F) (what makes "the
computations of (94) apply" in [Kol07, 95]).
The first derivative ideal transports along the Cohen isomorphism, Φ(D(J)) = D(Φ(J)).
The higher derivative ideals transport along the Cohen isomorphism.
The maximal contact ideal transports along the Cohen isomorphism, Φ(MC(J)) = MC(Φ(J)).
MC-invariance ([Kol07, 53]) of Î ⊆ R̂ in the completed coordinates transports to
MC-invariance of Φ⁻¹(Î) ⊆ K⟦X⟧ in the standard coordinates.
For Î ⊆ R̂ MC-invariant with MC(Î) ⊆ 𝔪R̂, the ideal Φ⁻¹(Î) of K⟦X⟧ is invariant under
every automorphism of the form 1 + Φ⁻¹(MC(Î)) ([Kol07, Proposition 94], (2) ⇒ (1), as applied
in [Kol07, 95]).
Kollár's "φ^* Î = Î" ([Kol07, 95]; [Kol07, Definition 91, (2)]), the equality
form: every automorphism g of the form 1 + Φ⁻¹(MC(Î)) satisfies g(Φ⁻¹ Î) = Φ⁻¹ Î.