Completions along flat local homomorphisms with trivial residue extension

The ring-theoretic content of "an étale map induces an isomorphism of completed local rings": Włodarczyk's "since φ is étale … Ô_{x',X'} ≃ Ô_{x,X}" (the proof of [Wlo05, Lemma 2.6.5]) and Kollár's "ψ is invertible after completion" (the discussion of [Kol07, Definition 91]). A flat local homomorphism φ : R →+* S with 𝔪_R S = 𝔪_S and trivial residue field extension induces a bijection R̂ → Ŝ of maximal-adic completions. The level maps R/𝔪_R^n → S/𝔪_S^n are

• injective: 𝔪_S^n = 𝔪_R^n S and φ is faithfully flat (Module.FaithfullyFlat.of_flat_of_isLocalHom), so 𝔪_R^n S ∩ R = 𝔪_R^n (Ideal.comap_map_eq_self_of_faithfullyFlat; comap_maximalIdeal_pow_of_flat);
• surjective: S = φ(R) + 𝔪_S (trivial residue extension) and 𝔪_S^n = 𝔪_R^n S give S = φ(R) + 𝔪_S^n for every n by induction (exists_sub_mem_maximalIdeal_pow, the graded step exists_mem_sub_mem_maximalIdeal_pow_succ);

and the completions are the limits: injectivity by AdicCompletion.ext_evalₐ, surjectivity by the right inverse completionInv assembled from the inverse level maps with AdicCompletion.liftRingHom. No Noetherian hypothesis is needed. In addition, completionMap φ carries I R̂ to φ(I) Ŝ (map_completionMap_map). These are the tools for passing from the formal to the étale case of the equivalence of hypersurfaces of maximal contact, where the key point, in Kollár's words, is "to realize the automorphism φ on some étale neighborhood" [Kol07, 95]; used in Hironaka/Scheme/Smooth/GraphCompletion.lean.

theorem IsLocalRing.map_maximalIdeal_pow_of_map_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (n : ℕ) : Ideal.map φ (maximalIdeal R ^ n) = maximalIdeal S ^ n

𝔪_S^n = 𝔪_R^n S when 𝔪_S = 𝔪_R S.

theorem IsLocalRing.comap_maximalIdeal_pow_of_flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (n : ℕ) : Ideal.comap φ (maximalIdeal S ^ n) = maximalIdeal R ^ n

For a flat local φ with 𝔪_R S = 𝔪_S, 𝔪_S^n ∩ R = 𝔪_R^n (faithful flatness).

theorem IsLocalRing.quotientMap_injective_of_flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (n : ℕ) : Function.Injective ⇑(Ideal.quotientMap (maximalIdeal S ^ n) φ ⋯)

The level map R/𝔪_R^n → S/𝔪_S^n is injective.

theorem IsLocalRing.exists_sub_mem_maximalIdeal_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hres : Function.Surjective ⇑(ResidueField.map φ)) (s : S) : ∃ (r : R), s - φ r ∈ maximalIdeal S

Trivial residue field extension: every element of S is congruent to an element of φ(R) modulo 𝔪_S.

theorem IsLocalRing.exists_mem_sub_mem_maximalIdeal_pow_succ {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) (n : ℕ) {m : S} (hmem : m ∈ maximalIdeal S ^ n) : ∃ r ∈ maximalIdeal R ^ n, m - φ r ∈ maximalIdeal S ^ (n + 1)

The graded step of the surjectivity of the level maps: an element of 𝔪_S^n = 𝔪_R^n S is congruent modulo 𝔪_S^(n+1) to the image of an element of 𝔪_R^n.

theorem IsLocalRing.exists_sub_mem_maximalIdeal_pow {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) (n : ℕ) (s : S) : ∃ (r : R), s - φ r ∈ maximalIdeal S ^ n

S = φ(R) + 𝔪_S^n for every n.

theorem IsLocalRing.quotientMap_surjective_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) (n : ℕ) : Function.Surjective ⇑(Ideal.quotientMap (maximalIdeal S ^ n) φ ⋯)

The level map R/𝔪_R^n → S/𝔪_S^n is surjective.

theorem IsLocalRing.factorPow_comp_quotientMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] {m n : ℕ} (hle : m ≤ n) : (Ideal.Quotient.factorPow (maximalIdeal S) hle).comp (Ideal.quotientMap (maximalIdeal S ^ n) φ ⋯) = (Ideal.quotientMap (maximalIdeal S ^ m) φ ⋯).comp (Ideal.Quotient.factorPow (maximalIdeal R) hle)

The level maps commute with the transition maps of the two completions.

theorem IsLocalRing.completionMap_injective_of_flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) : Function.Injective ⇑(completionMap φ)

R̂ → Ŝ is injective (injective level maps, ext_evalₐ).

noncomputable def IsLocalRing.completionInvLevel {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) (n : ℕ) : AdicCompletion (maximalIdeal S) S →+* R ⧸ maximalIdeal R ^ n

The level-n inverse Ŝ → S/𝔪_S^n → R/𝔪_R^n of the bijective level map.

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalRing.quotientMap_completionInvLevel {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) (n : ℕ) (y : AdicCompletion (maximalIdeal S) S) : (Ideal.quotientMap (maximalIdeal S ^ n) φ ⋯) ((completionInvLevel φ hflat hm hres n) y) = (AdicCompletion.evalₐ (maximalIdeal S) n) y

theorem IsLocalRing.completionInvLevel_compat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) {m n : ℕ} (hle : m ≤ n) : (Ideal.Quotient.factorPow (maximalIdeal R) hle).comp (completionInvLevel φ hflat hm hres n) = completionInvLevel φ hflat hm hres m

noncomputable def IsLocalRing.completionInv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) : AdicCompletion (maximalIdeal S) S →+* AdicCompletion (maximalIdeal R) R

The inverse Ŝ → R̂, assembled from the inverse level maps.

Equations

• IsLocalRing.completionInv φ hflat hm hres = AdicCompletion.liftRingHom (IsLocalRing.maximalIdeal R) (IsLocalRing.completionInvLevel φ hflat hm hres) ⋯

theorem IsLocalRing.completionMap_completionInv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Surjective ⇑(ResidueField.map φ)) (y : AdicCompletion (maximalIdeal S) S) : (completionMap φ) ((completionInv φ hflat hm hres) y) = y

theorem IsLocalRing.bijective_completionMap_of_flat_of_map_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (hflat : φ.Flat) (hm : Ideal.map φ (maximalIdeal R) = maximalIdeal S) (hres : Function.Bijective ⇑(ResidueField.map φ)) : Function.Bijective ⇑(completionMap φ)

A flat local homomorphism φ : R →+* S of local rings with 𝔪_R S = 𝔪_S and trivial residue field extension induces a bijection R̂ → Ŝ of maximal-adic completions (the ring form of "étale maps are invertible after completion", [Kol07, Definition 91]; the proof of [Wlo05, Lemma 2.6.5]).

theorem IsLocalRing.map_completionMap_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (I : Ideal R) : Ideal.map (completionMap φ) (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I) = Ideal.map (algebraMap S (AdicCompletion (maximalIdeal S) S)) (Ideal.map φ I)

The induced map on completions carries the extension I R̂ of an ideal to the extension φ(I) Ŝ of its image.