K-algebra endomorphisms of K⟦X₁, …, Xₙ⟧ preserving the maximal ideal #
Kollár, in the proof of the formal equivalence theorem: "(91.4) is also clear" [Kol07, 95], that is,
[Kol07, Definition 91, (4)]: for the automorphism φ^* of Ô_{p,X} ≅ K⟦x⟧ of the form 1 + B,
h − φ^*(h) ∈ B for every h.
The underlying fact for R = K⟦x⟧: if σ is a K-algebra endomorphism of R and B ⊆ 𝔪 an
ideal with σ(Xᵢ) − Xᵢ ∈ B for all i, then σ(h) − h ∈ B for all h ∈ R
(sub_map_mem_of_forall_sub_X_mem).
Why it holds. A K-algebra endomorphism σ with σ(Xᵢ) ∈ 𝔪 maps 𝔪 = (X₁, …, Xₙ) into 𝔪
(the generators go into 𝔪), hence 𝔪^N into 𝔪^N for every N
(mem_maximalIdeal_pow_map_of_forall_X_mem). For a polynomial P, σ(P) − P ∈ B by induction on
P: constants are fixed (K-linearity), sums add, and
σ(P·Xᵢ) − P·Xᵢ = (σP − P)·σ(Xᵢ) + P·(σ(Xᵢ) − Xᵢ). For a power series h and each N, write
h = P + G with P = truncTotal (N+1) h a polynomial and G ∈ 𝔪^{N+1} (sub_truncTotal_mem of
Hironaka/Algebra/Local/Taylor.lean); then σ(h) − h = (σP − P) + (σG − G) ∈ B + 𝔪^N, and Krull's
intersection theorem (mem_of_forall_mem_sup_pow: B = ⋂_N (B + 𝔪^N) in the Noetherian local
ring K⟦X⟧) gives σ(h) − h ∈ B. No continuity of σ is assumed: preservation of the powers of
𝔪 is automatic from σ(Xᵢ) ∈ 𝔪.
The same approximation shows that such a σ is a substitution
(eq_substAlgHom_of_forall_X_mem): σ and substAlgHom (σ ∘ X) are K-algebra maps agreeing on
the Xᵢ, hence on polynomials, and both map 𝔪^{N+1} into 𝔪^{N+1}, so they agree modulo every
𝔪^N, hence everywhere. This is the form in which the transported automorphism Φ'⁻¹ ∘ Φ of
two Cohen isomorphisms is fed to IsOnePlus of Hironaka/Algebra/Local/FormalAut.lean (whose first
clause asks for a substitution) — Kollár's description of the automorphisms of K⟦x⟧ as the
substitutions xᵢ ↦ gᵢ [Kol07, Notation 93].
A power series lies in the maximal ideal of K⟦X⟧ iff its constant coefficient vanishes.
Xᵢ ∈ 𝔪.
A K-algebra endomorphism sending every Xᵢ into 𝔪 maps 𝔪 into 𝔪.
Such a σ maps 𝔪^N into 𝔪^N.
Two K-algebra endomorphisms of K⟦X⟧ agreeing on the variables agree on polynomials.
For an ideal B ⊆ 𝔪 of K⟦X₁, …, Xₙ⟧ and a K-algebra endomorphism σ with σ(Xᵢ) − Xᵢ ∈ B
for every i, σ(h) − h ∈ B for every power series h (Kollár's "(91.4) is also clear",
[Kol07, 95], for [Kol07, Definition 91, (4)]): on polynomials by induction, on power series by
approximation modulo 𝔪^N and
Krull's intersection theorem.
The substitution family Xᵢ ↦ σ(Xᵢ) of a K-algebra endomorphism sending the variables into
𝔪 (the xᵢ ↦ gᵢ of [Kol07, Notation 93]).
A K-algebra endomorphism σ of K⟦X⟧ sending every Xᵢ into 𝔪 is the substitution
Xᵢ ↦ σ(Xᵢ) [Kol07, Notation 93] — both agree on polynomials and both map 𝔪^{N+1} into
itself, so they agree modulo every 𝔪^N. (Compare continuous_iff_exists_substAlgHom of
Hironaka/Algebra/Local/FormalAut.lean, which needs continuity instead.)
Two K-algebra endomorphisms of K⟦X⟧ sending the variables into 𝔪 and agreeing on the
variables are equal (both are the substitution by their common values).