Completions of an étale neighbourhood pair #
Kollár: for an étale neighbourhood pair ψ, ψ', "ψ is invertible after completion", and
φ := ψ̂' ∘ ψ̂⁻¹ : X̂ → X̂ is the automorphism sought (the remark after [Kol07, Definition 91]);
for the graph of two
coordinate systems, φ_p^*(x_1', x_2, …) = (x_1, x_2, …) and φ^* Î = Î ([Kol07, 95], the proof
of Theorem 92). Włodarczyk: an étale φ induces Ô_{x',X'} ≅ Ô_{x,X} (the proof of Wlo05,
Lemma 2.6.5).
bijective_completionMap_stalkMap: an étaleψ : W ⟶ Ywithκ(q) = κ(ψ(q))induces a bijectionÔ_{Y,ψ(q)} → Ô_{W,q}: the stalk map is flat (Flat.stalkMap), carries𝔪_{ψ(q)}onto𝔪_q(map_maximalIdeal_stalkMap_of_etale, unramifiedness) and is bijective on residue fields, so the ring formbijective_completionMap_of_flat_of_map_maximalIdeal(Hironaka/Algebra/Local/CompletionEtale.lean) applies.bijective_completionMap_stalkHom,…stalkHom',formalAutomorphism_germ,formalAutomorphism_cohenEquivOfResidue_X: for an étale neighbourhood pairQbothψ̂^*andψ̂'^*are bijective (the previous item composed with the transport alongψ(q) = p), and for the pairPof two coordinate systems the formal automorphismφ = (ψ̂'^*)⁻¹ ∘ ψ̂^*sendsû_itov̂_i:ψ̂'^*(φ(û_i)) = ψ̂^*(û_i)is the germ atqofψ^*(u_i) = ψ'^*(v_i)(graphFst_appTop_eq) andψ̂'^*is injective. Under the Cohen isomorphismκ(p)⟦x⟧ ≅ Ô_{X,p}withx_i ↦ û_i(cohenMap_X,Hironaka/Algebra/Local/CohenIso.lean) this readsφ(x_i) = v̂_i.map_completionMap_stalkHom,…stalkHom',map_adicCompletion_stalkIdeal_comap_eq_iff:ψ̂^*(Î_p) = (ψ^*I)^_q, since the stalk of the pulled-back ideal sheaf is the extension of the stalk (stalkIdeal_comap) and completion commutes with extension of ideals (map_completionMap_map); so(ψ^*I)^_q = (ψ'^*I)^_qiffφ(Î_p) = Î_p.
The germ computation germ_stalkHom (ψ^* of the germ at p of a section of U is the germ at
q of ψ^*(s)) goes through Mathlib's Scheme.Hom.germ_stalkMap_apply and the transport of germs
along stalkCongr (stalkCongr_germ). These are the steps from the étale pair to the formal
automorphism of [Kol07, Definition 91]
(Hironaka/Resolution/Algebraic/MaximalContact/EtaleToFormal.lean).
An étale morphism ψ : W ⟶ Y with κ(q) = κ(ψ(q)) induces an isomorphism
Ô_{Y,ψ(q)} ≅ Ô_{W,q} ("ψ is invertible after completion", the remark after
[Kol07, Definition 91]; the proof of [Wlo05, Lemma 2.6.5]).
The transport of stalks along an equality of points, on germs.
The transport of stalks along an equality of points carries the stalk of an ideal sheaf to the stalk of the same ideal sheaf.
ψ̂^* : Ô_{X,p} → Ô_{W,q} is bijective for an étale neighbourhood pair.
ψ̂'^* : Ô_{X,p} → Ô_{W,q} is bijective for an étale neighbourhood pair.
ψ^* on germs: the germ at p of a section s over V ∋ p goes to the germ at q of
ψ^*(s).
ψ'^* on germs.
ψ̂^*(Î_p) = (ψ^*I)^_q: the completion of the stalk of I is carried to the completion of
the stalk of the pulled-back ideal sheaf.
ψ̂'^*(Î_p) = (ψ'^*I)^_q.
ψ^*I and ψ'^*I have equal completions at q iff the formal automorphism preserves Î_p
(Kollár's "φ^* Î = Î", [Kol07, 95]).
The germ at x ∈ V of a section of X over V, pushed to the stalk of the open subscheme
V along V.ι, is the germ of the same section read as a global section of V.
For a pair landing in U, ψ^* of the germ at p of a section s of U is the germ at
q of ψ^*(s) (with s read as a global section of U through topIso).
ψ'^* on germs, for a pair landing in U.
The formal automorphism of a pair for the coordinate data u, v sends the completed germ of
u_i to that of v_i (Kollár's φ_p^*(x_1', x_2, …) = (x_1, x_2, …), [Kol07, 95]; Włodarczyk's
functions w_i, the proof of [Wlo05, Lemma 2.9.5]).
The Cohen form: under κ(p)⟦x⟧ ≅ Ô_{X,p} with x_i ↦ û_i (cohenEquivOfResidue), the formal
automorphism is x_i ↦ v̂_i (Kollár's "Ô_{p,X} ≅ K⟦x_1, …, x_n⟧ by (55), so the computations of
(94) apply", [Kol07, 95]).