From étale equivalence to formal equivalence #
[Kol07, Definition 91] ends by noting that ψ is invertible after completion, so that
"φ := ψ̂' ∘ ψ̂⁻¹ : X̂ → X̂ is the automorphism we seek". This file proves the statement behind
that sentence: if ψ(u) = ψ'(u) = p with ψ, ψ' étale and
trivial residue field extensions at u, then ψ̂, ψ̂' : Ô_{p,X} → Ô_{u,U} are isomorphisms and φ
is a formal equivalence at p whenever (1′)–(4′) hold on a neighbourhood of u.
The setting. A point u ∈ U over p along both maps with κ(u) = κ(p) is an
EtaleNbhdPair X p (W := U, q := u); its stalkHom, stalkHom' are the local homomorphisms
ψ^*, ψ'^* : 𝒪_{X,p} → 𝒪_{U,u}, whose completions ψ̂, ψ̂' are bijective
(bijective_completionMap_stalkHom). On functions Kollár's φ is the k-algebra automorphism
φ^* := ψ̂⁻¹ ∘ ψ̂' of Ô_{X,p}, the inverse of formalAutomorphism = ψ̂'⁻¹ ∘ ψ̂, so that (91.1)
reads φ^*(Ĥ') = Ĥ exactly from (1′) ψ⁻¹(H) = ψ'⁻¹(H').
- (91.1)–(91.3) are transports of ideals:
map_completionMap_stalkHomgivesψ̂(Ĵ) = (ψ^*J)^for every ideal sheafJ(and the same forψ'), soφ^*(Ĵ') = ψ̂⁻¹(ψ̂'(Ĵ')) = ψ̂⁻¹((ψ'^*J')^) = ψ̂⁻¹((ψ^*J)^) = Ĵwheneverψ^*J = ψ'^*J'(map_formalAutomorphism_symm_completionIdeal, applied to (1′), (2′), (3′)). k-linearity.ψ ≫ f = ψ' ≫ f(Kollár's maps ofk-varieties, the fieldcomp_eqofEtaleEquiv):ψ^*andψ'^*both carry thek-structure of𝒪_{X,p}induced byfto the one of𝒪_{U,u}induced byψ ≫ f = ψ' ≫ f(stalkHom_algebraMap), soψ̂'(c) = ψ̂(c)forc ∈ kandφ^*fixesk(formalAutomorphism_symm_algebraMap).- (91.4) is the substance. By [Kol07, Lemma 74 (4)]
MC(ψ^*I) = ψ^*MC(I)(MC_comap_of_etale), so (4′) saysψ ∘ ι = ψ' ∘ ιonV(M)forM := ψ^*MC(I), and we needĥ − φ^*ĥ ∈ MC(I)^for everyĥ ∈ Ô_{X,p}, i.e. (applying the injectiveψ̂and the transport)ψ̂ĥ − ψ̂'ĥ ∈ M̂ := M_u Ô_{U,u}.- Stalk step (Kollár's own reading of (4′), "
ψ^*(h) − ψ'^*(h) ∈ MC ψ^*(I)"): fora ∈ 𝒪_{X,p},ψ^*a − ψ'^*a ∈ M_u. Ifu ∉ V(M)thenM_u = 𝒪_{U,u}; otherwiseu = ι(z), the kernel ofι^* : 𝒪_{U,u} → 𝒪_{V(M),z}isM_u(ker_stalkMap_subschemeι), and on a sectionsrepresentinga,ι^*ψ^*s = (ψ ∘ ι)^*s = (ψ' ∘ ι)^*s = ι^*ψ'^*s(germ_app_sub_germ_app_mem_stalkIdeal). - Completion step (not in the sources):
ĥagrees with somea ∈ 𝒪_{X,p}to ordern(ĥ − a ∈ 𝔪̂ⁿ;Ô = lim 𝒪/𝔪ⁿ, [Kol07, Definition 55]), andψ̂, ψ̂'preserve the powers of the maximal ideals, soψ̂ĥ − ψ̂'ĥ ∈ M̂ + 𝔪̂_Uⁿfor everyn. The idealM̂ = M_u Ô_{U,u}is closed in the𝔪̂-adic topology of the completion of the Noetherian local ring𝒪_{U,u}, the Krull-intersection remark of [Kol07, Definition 55] in the form: completion is exact on finite modules (Artin–Rees, Mathlib'sAdicCompletion.map_exact), soM̂is the kernel ofÔ_{U,u} → (𝒪_{U,u}/M_u)^, and the target is Hausdorff (mem_map_algebraMap_adicCompletion_of_forall).
- Stalk step (Kollár's own reading of (4′), "
Two forms are proved: formallyEquivalentAt_of_etaleNbhdPair, the neighbourhood form on an
EtaleNbhdPair with (1′)–(4′) (the graph neighbourhood U₁(p) in the proof of Theorem 92 is
such a pair and need not cover the cosupport), and formallyEquivalentAt_of_etaleEquiv for an
étale equivalence Q : EtaleEquiv f I m E H H' and a point u ∈ U over p.
Ô = lim 𝒪/𝔪ⁿ ([Kol07, Definition 55]): every element of the completion Ŝ of a Noetherian
local ring agrees with an element of S to any prescribed order, x − a ∈ 𝔪̂ⁿ.
The Krull-intersection remark of [Kol07, Definition 55]: the extension JŜ of an ideal J of
a Noetherian local ring S to the completion Ŝ is closed, i.e. an element of Ŝ lying in
JŜ + 𝔪̂ⁿ for every n lies in JŜ. Proof: completion is exact on finitely generated modules
(Artin–Rees, Mathlib's AdicCompletion.map_exact), so JŜ (the image of the completion of J,
range_adicCompletion_map_subtype) is the kernel of Ŝ → (S/J)^, and (S/J)^ is 𝔪-adically
Hausdorff.
Kollár's reading of (4′), "ψ^*(h) − ψ'^*(h) ∈ MC ψ^*(I) for every h ∈ 𝒪_X"
([Kol07, Definition 91]), at a point of the support: if ψ, ψ' : W ⟶ X agree on the closed
subscheme V(M) (AgreeOn) and w ∈ V(M), the germs at w of ψ^*s and ψ'^*s differ by an
element of the stalk M_w, for every section s of 𝒪_X near ψ(w) = ψ'(w). Proof: w = ι(z)
for the closed immersion ι : V(M) ⟶ W, whose stalk map at z has kernel M_w
(ker_stalkMap_subschemeι), and ι^*ψ^*s = (ι ≫ ψ)^*s = (ι ≫ ψ')^*s = ι^*ψ'^*s.
The condition (4′) read on the stalks at q: for an étale neighbourhood pair Q of p whose
maps agree on V(M), ψ^*a − ψ'^*a ∈ M_q for every a ∈ 𝒪_{X,p}. Off the support of M the
stalk M_q is the whole ring (mem_support_iff_stalkIdeal_le_maximalIdeal); on it,
germ_app_sub_germ_app_mem_stalkIdeal on a representing section (stalkHom_germ).
The condition (4′) for elements of the completion: for an étale neighbourhood pair Q of p
on a locally Noetherian X whose maps agree on V(M), ψ̂ĥ − ψ̂'ĥ ∈ M_q Ô_{W,q} for every
ĥ ∈ Ô_{X,p}. Approximate ĥ by a ∈ 𝒪_{X,p} to order n
(exists_sub_algebraMap_mem_maximalIdeal_pow), use stalkHom_sub_stalkHom'_mem for a and the
preservation of 𝔪̂ⁿ by ψ̂, ψ̂' (completionMap_mem_maximalIdeal_pow), and close with
mem_map_algebraMap_adicCompletion_of_forall.
Kollár's ψ : U → X is a morphism of k-varieties: ψ^* carries the k-structure of
𝒪_{X,p} induced by f : X ⟶ Spec k (stalkAlgebra) to the one of 𝒪_{W,q} induced by
ψ ≫ f.
stalkHom_algebraMap for the second map ψ'.
Kollár's ψ, ψ' : U ⇉ X are morphisms of k-varieties (EtaleEquiv.comp_eq): when
ψ ≫ f = ψ' ≫ f, ψ^* and ψ'^* agree on the constants k ⊆ 𝒪_{X,p}.
Kollár's φ := ψ̂' ∘ ψ̂⁻¹ read on functions: the inverse of formalAutomorphism is
φ^* = ψ̂⁻¹ ∘ ψ̂', i.e. ψ̂ ∘ φ^* = ψ̂'.
φ is an automorphism of X̂ = Spec_k Ô_{p,X} over k: for ψ ≫ f = ψ' ≫ f,
φ^* = ψ̂⁻¹ ∘ ψ̂' fixes the constants k ⊆ Ô_{X,p} (the k-structure of FormallyEquivalentAt,
f.stalkAlgebra p extended to the completion).
The conditions (91.1)–(91.3) of [Kol07, Definition 91] from (1′)–(3′): if ψ^*J = ψ'^*J' then
φ^*(Ĵ') = Ĵ for φ^* = ψ̂⁻¹ ∘ ψ̂', by the transports ψ̂(Ĵ) = (ψ^*J)^, ψ̂'(Ĵ') = (ψ'^*J')^ and
the injectivity of ψ̂. With J = H, J' = H' this is (91.1); with J = J' = I (91.2); with
J = J' = Eⁱ (91.3).
The condition (91.4) of [Kol07, Definition 91] from (4′): if ψ, ψ' agree on V(ψ^*M) then
ĥ − φ^*ĥ ∈ M̂ for every ĥ ∈ Ô_{X,p}, for φ^* = ψ̂⁻¹ ∘ ψ̂': apply the injective ψ̂, transport
ψ̂(M̂) = (ψ^*M)^ and use completionMap_stalkHom_sub_mem.
Kollár's "φ := ψ̂' ∘ ψ̂⁻¹ : X̂ → X̂ is the automorphism we seek" ([Kol07, Definition 91]), in
neighbourhood form: for X smooth over k and
an étale neighbourhood pair Q of p (EtaleNbhdPair: ψ, ψ' : W ⟶ X étale, ψ(q) = ψ'(q) = p,
trivial residue field extensions at q) with ψ ≫ f = ψ' ≫ f and (1′)–(4′) on W, H and H'
are formally equivalent at p with respect to (X, I, E) (FormallyEquivalentAt), through the
k-automorphism φ^* = ψ̂⁻¹ ∘ ψ̂' of Ô_{X,p}. X and W are locally Noetherian (X of finite
type over k, ψ étale); (91.1)–(91.3) are map_formalAutomorphism_symm_completionIdeal, (91.4)
is sub_formalAutomorphism_symm_mem with MC(ψ^*I) = ψ^*MC(I) (MC_comap_of_etale).
For an étale equivalence Q of H and H' with respect to (X, I, E) and a point u ∈ U
with ψ(u) = ψ'(u) = p and trivial residue field extensions at u, H and H' are formally
equivalent at p: formallyEquivalentAt_of_etaleNbhdPair for the neighbourhood pair
(U, u, ψ, ψ') with Q's conditions (1′)–(4′) and comp_eq.