Uniqueness of algebra maps into a separated local ring with equal residues

Kollár constructs a field of representatives k' ⊂ Ô_{p,X} of the residue field κ(p) of a closed point by Hensel's lemma [Kol07, Definition 55]: the existence of a coefficient field over k. The study of formal equivalence of points also needs the complementary uniqueness: two k-algebra homomorphisms κ(p) → Ô_{p,X} with the same residue composite coincide. This module proves the ring-level statement behind it; it is not in the sources.

The argument

Let A be a formally unramified k-algebra (for a field extension κ(p)/k this is separability, Mathlib's Algebra.FormallyUnramified.of_isSeparable), B a local k-algebra separated for the 𝔪-adic topology (IsHausdorff (maximalIdeal B) B, i.e. ⋂ₙ 𝔪ⁿ = 0; Krull's intersection theorem for Noetherian local rings, an instance for adic completions) and σ₁, σ₂ : A →ₐ[k] B with σ₁ ≡ σ₂ modulo the maximal ideal 𝔪 (equal residues). Then σ₁ ≡ σ₂ modulo every 𝔪ⁿ: if the two maps agree modulo 𝔪ⁿ, they agree modulo 𝔪ⁿ⁺¹, because the ideal 𝔪ⁿ/𝔪ⁿ⁺¹ of B/𝔪ⁿ⁺¹ has square zero and formal unramifiedness says that two maps into B/𝔪ⁿ⁺¹ agreeing modulo a square-zero ideal are equal (Algebra.FormallyUnramified.comp_injective). Separatedness (IsHausdorff.haus) then gives σ₁ a − σ₂ a ∈ ⋂ₙ 𝔪ⁿ = 0.

The lemma is stated for any 𝔪-adically separated local ring B. It is applied to B = Ô_{p,X}, the completion of the Noetherian stalk at a closed point (𝔪̂-adically complete by Mathlib's instance), and A = κ(p), algebraic over k of characteristic zero and hence formally unramified: a residue-trivial k-automorphism of Ô_{p,X} ≅ κ(p)⟦x₁, …, xₙ⟧ is then determined by its values on the coordinates, which is how the completion of the graph of a formal isomorphism between two points is identified.

theorem IsLocalRing.algHom_ext_of_residue_eq {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra.FormallyUnramified k A] [IsLocalRing B] [IsHausdorff (maximalIdeal B) B] (σ₁ σ₂ : A →ₐ[k] B) (h : ∀ (a : A), (residue B) (σ₁ a) = (residue B) (σ₂ a)) : σ₁ = σ₂

Two k-algebra homomorphisms from a formally unramified k-algebra A into an 𝔪-adically separated local k-algebra B with the same residue composite are equal: the uniqueness complementing the Hensel-lemma construction of a field of representatives [Kol07, Definition 55]; not in the sources. Induction along the powers of the maximal ideal with Algebra.FormallyUnramified.comp_injective for the square-zero ideals 𝔪ⁿ/𝔪ⁿ⁺¹, then separatedness (Krull's intersection theorem).