The completion of U₁(p) at (p, p) is the graph of φₚ #
The sentence of [Kol07, 95] "The completion of U₁(p) at (p, p) is the graph of φₚ", made
precise for an étale neighbourhood pair ψ, ψ' : W ⇉ X of the graph of the two coordinate
systems: the automorphism φ := (ψ̂^*)⁻¹ ∘ ψ̂'^* of Ô_{X,p} (EtaleNbhdPair.formalAutomorphism,
inverted) satisfies the conditions (91.1)–(91.4) of [Kol07, Definition 91], so it is the
automorphism of the formal half of Theorem 92
(Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivExists.lean) and the completed graph is
its graph. This is the step of the proof of Theorem 92
(Hironaka/Resolution/Algebraic/MaximalContact/Theorem92.lean) that passes from the formal
automorphism to the étale neighbourhood.
The coefficient field #
The first ingredient is the uniqueness of the k-linear coefficient field of Ô_{X,p} at a
closed point (coefficientField_ext): κ(p)/k is algebraic, hence separable in characteristic
zero and formally unramified, and Ô_{X,p} is a Noetherian local ring, so
IsLocalRing.algHom_ext_of_residue_eq applies. This is what pins a residue-trivial
k-automorphism of Ô_{X,p} ≅ κ(p)⟦X⟧ by its values on the coordinates: it must fix the
coefficient field, hence is κ(p)-linear on the chart. k-linearity alone would not pin it: an
automorphism of κ(p) over k applied to the coefficients is k-linear, fixes the coordinates
and is not the identity.
Uniqueness of the field of representatives over k (the subfield k' ⊂ Ô_{p,X} of
[Kol07, Definition 55]): two k-algebra homomorphisms κ(p) → Ô_{X,p} at a closed point p with
the same residue composite are equal. κ(p)/k is algebraic
(isAlgebraic_residueField_of_isClosed), hence separable and formally unramified in characteristic
zero, and Ô_{X,p} is Noetherian local: IsLocalRing.algHom_ext_of_residue_eq.
Kollár's "The completion of U₁(p) at (p, p) is the graph of φₚ" ([Kol07, 95]): for a
closed point p of cosupp(I, m), m ≥ 1, I MC-invariant, coordinates x₁, x₁' ∈ MC(I)_p with
H_p = (x₁), H'_p = (x₁'), (x₁', y) a regular system and every Eⁱ through p equal to
(y_j), and an étale neighbourhood pair Q of p over k with ψ^*(s) − ψ'^*(s) ∈ 𝔪_q and the
graph equations ψ^*((x₁, y)ᵢ) = ψ'^*((x₁', y)ᵢ), the automorphism φ := θ⁻¹ = (ψ̂^*)⁻¹ ∘ ψ̂'^* of
Ô_{X,p} satisfies (91.1)–(91.4). Proof: φ is k-linear, sends x̂₁' ↦ x̂₁ and ŷⱼ ↦ ŷⱼ (the
graph equations through ψ̂^*, ψ̂'^*), and is trivial modulo 𝔪̂ (the residue condition,
completed), hence fixes the k-linear coefficient field of the chart Φ' of (x₁', y)
(coefficientField_ext); on the chart it is therefore a κ(p)-substitution
X₀ ↦ X₀ + Φ'⁻¹(x̂₁ − x̂₁'), Xᵢ ↦ Xᵢ, of the form 1 + Φ'⁻¹(\widehat{MC(I)}), the shape of
exists_formalAutomorphism; (91.2) is then map_comap_completionIdeal_eq_of_isOnePlus
([Kol07, Proposition 94]), (91.4) the calculus of substitutions 1 + B, (91.1) and (91.3)
map_completionIdeal_eq_of_stalkIdeal_eq_span.