Theorem 92, the formal half: formal equivalence at a closed point of the cosupport #
The formal part of the proof of [Kol07, Theorem 92], which is [Kol07, 95], assembled from: the
coordinates x₁, x₁' ∈ MC(I)_p, y = (x₂, …, xₙ)
(Hironaka/Resolution/Algebraic/MaximalContact/Coordinates.lean), the k-linear Cohen isomorphisms
(Hironaka/Algebra/Local/CoefficientFieldOver.lean), [Kol07, Proposition 94] on the chart
(Hironaka/Algebra/Local/CohenDerivation.lean) with its stalk-level inputs
(Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivBridge.lean), the completed principal
ideals (Hironaka/Resolution/Algebraic/MaximalContact/CompletionIdealMap.lean) and the calculus of
substitutions of the form 1 + B (Hironaka/Algebra/Local/PowerSeriesEndomorphism.lean).
Why it holds. At a closed point p ∈ cosupp(I, m) take Kollár's coordinates
x₁, x₁' ∈ MC(I)_p, y = (x₂, …, xₙ) and the chart Φ' : κ(p)⟦X⟧ ≃ₐ[k] Ô_{X,p} of (x₁', y) for
a coefficient field σ.
- The automorphism on the chart (
exists_formalAutomorphism): the chartΦof(x₁, y)for the sameσgivesg := Φ'⁻¹ ∘ Φ, aκ(p)-algebra automorphism ofκ(p)⟦X⟧(it fixes the constants) withg(X₀) = Φ'⁻¹(ι x₁) = X₀ + Φ'⁻¹(ι(x₁ − x₁'))andg(Xᵢ₊₁) = Xᵢ₊₁, Kollár'sφ^*(x₁', x₂, …) = (x₁' + (x₁ − x₁'), x₂, …); it is a substitution because it sends theXᵢinto𝔪([Kol07, Notation 93]), and of the form1 + Φ'⁻¹(\widehat{MC(I)})becausex₁ − x₁' ∈ MC(I)_p. - Invariance of
Î(isInvariantOnePlus_comap_completionIdeal,map_comap_completionIdeal_eq_of_isOnePlus): any chart sending the variables to a prescribed regular system of parameters and the constants to a coefficient field is the Cohen isomorphism of coordinates adapted to that regular system (cohenAlgEquiv_eq,exists_regularCoords_eq), for which the ring-level Proposition 94 applies; the inputs are MC-invariance ofÎin the completed coordinates and\widehat{MC(I)} ⊆ 𝔪Ô. - Assembly (
formallyEquivalentAt_of_isMCInvariant):φ := Φ' ∘ g ∘ Φ'⁻¹is ak-algebra automorphism ofÔ_{X,p}(Φ'isk-linear,gisκ(p)- hencek-linear). (91.1):φ(ι x₁') = ι x₁, soφ(Ĥ') = Ĥ; (91.2):g(Φ'⁻¹ Î) = Φ'⁻¹ Îtransports toφ(Î) = Î; (91.3):φ(ι yⱼ) = ι yⱼfixes the completed equations of theEⁱthroughp, and those not throughphave unit completed ideal; (91.4):g(F) − F ∈ Φ'⁻¹(\widehat{MC(I)})for allF, soh − φ(h) ∈ \widehat{MC(I)}for allh. That is [Kol07, Definition 91] (FormallyEquivalentAt).
The invariance statement is used again in
Hironaka/Resolution/Algebraic/MaximalContact/GraphOfAutomorphism.lean, where the automorphism of
Ô_{X,p} induced by an étale neighbourhood of the graph is shown to satisfy (91.2), on the way to
the étale half of Theorem 92 (Hironaka/Resolution/Algebraic/MaximalContact/Theorem92.lean).
Membership in the maximal ideal is transported along a k-algebra isomorphism of the
completion with κ(p)⟦X⟧.
The canonical image of an element of 𝔪_p lies in the maximal ideal of the completion.
Kollár's automorphism in [Kol07, 95], on the chart Φ' of (x₁', y):
φ^*(x₁', x₂, …, xₙ) = (x₁' + (x₁ − x₁'), x₂, …, xₙ) is a κ(p)-algebra automorphism of κ(p)⟦X⟧
of the form 1 + Φ'⁻¹(\widehat{MC(I)}) with g(X₀) = X₀ + Φ'⁻¹(ι(x₁ − x₁')) and
g(Xᵢ₊₁) = Xᵢ₊₁, namely Φ'⁻¹ ∘ Φ for the chart Φ of (x₁, y) with the same constants
([Kol07, Notation 93]).
[Kol07, Proposition 94 (1)] at the stalk, as used in [Kol07, 95]: for I MC-invariant, p a
closed point of cosupp(I, m), m ≥ 1, and a k-linear chart Φ sending the variables to a
regular system of parameters z and the constants to a coefficient field, the ideal Φ⁻¹(Î) of
κ(p)⟦X⟧ is invariant under every automorphism of the form 1 + Φ⁻¹(\widehat{MC(I)}).
Kollár's φ^* Î = Î in [Kol07, 95], condition (91.2), in equality form: every automorphism g
of the form 1 + Φ⁻¹(\widehat{MC(I)}) satisfies g(Φ⁻¹ Î) = Φ⁻¹ Î.
The formal half of [Kol07, Theorem 92] ([Kol07, 95]): under the hypotheses of Theorem 92,
H and H' are formally equivalent at every closed point p ∈ cosupp(I, m) with respect to
(X, I, E).