A local homomorphism inducing an isomorphism of completions #
A bijectivity criterion for the map of completions  → B̂ induced by a local homomorphism
f : A → B of Noetherian local rings, through the Cohen structure theorem
(completionMap_bijective_of_cohen). Given a coefficient field on  and a regular system of
parameters y of A, so that Ψ : K_A⟦X⟧ ≃ Â (cohenEquivOfResidue,
Hironaka/Algebra/Local/CohenIso.lean), and an isomorphism Θ : B̂ ≃ K⟦X⟧ with Θ(f(yᵢ)) = Xᵢ
such that Θ ∘ f̂ carries the coefficient field to the constants through a bijection e : K_A → K,
the composite Θ ∘ f̂ ∘ Ψ : K_A⟦X⟧ → K⟦X⟧ is the coefficient map F ↦ F.map e: both sides agree,
level by level, with the evaluation of the truncation truncTotal N F modulo 𝔪ᴺ (mk_cohenMap).
Hence f̂ is bijective.
Also here: a ring map c : K → A from a field with a local retraction ev : A → K identifies K
with the residue field of A, and K → A → Â is then a coefficient field of Â, a section of the
residue map in the sense of [Kol07, Definition 55] (isCoefficientAlgebra_of_section); this is the
situation of [BM97, (0.1)(2)], where the residue field is contained in the completion. Coefficient
maps of power series along a bijection are bijections (mvPowerSeries_map_bijective).
Applied in Hironaka/Manifold/BlowUp/Transform/StrictSubspaceCompletion.lean, an input to the
proof there of [BM97, Proposition 3.13] on the strict transform, to the map R'_{𝔪'} → 𝒪_{M',a'}
from the local ring of the chart ring to the ring of germs of analytic functions at a point of the
exceptional divisor, with the constants as the coefficient field and the Taylor isomorphism
𝒪̂_{M',a'} ≅ 𝕜⟦X⟧ as Θ. The criterion itself is not stated in the sources.
Coefficient maps of power series along a bijection are bijections.
Constants as a coefficient field ([Kol07, Definition 55]): a ring map c : K → A from a
field with a local retraction ev : A → K (ev ∘ c = id) identifies K with the residue field of
A, and K → A → Â is a coefficient field of Â, a section of the residue map.
Bijectivity of the induced map of completions through Cohen structure: for a local
homomorphism f : A → B, a regular system of parameters y of A, a coefficient field on Â,
and an isomorphism Θ : B̂ ≃ K⟦X⟧ with Θ(f(yᵢ)) = Xᵢ and Θ(f̂(k)) = e(k) for a bijection
e : K_A → K of the coefficient fields, f̂ : Â → B̂ is bijective: Θ ∘ f̂ ∘ Ψ is the coefficient
map F ↦ F.map e.