The map induced on maximal-adic completions by a local homomorphism

Kollár writes the chart map of a blow-up in power series, f ↦ f(y₁y_r, …, y_{r-1}y_r, y_r, …, yₙ) [Kol07, Definition 60, (60.3)], which is the map induced on completions by the local homomorphism R → R'_{𝔪'} from the base to the local ring of the chart. Mathlib has the functoriality of AdicCompletion in the module (AdicCompletion.map, same ring) and the universal property of a completion for maps into it (AdicCompletion.liftRingHom: a compatible family R →+* S ⧸ Iⁿ lifts to R →+* AdicCompletion I S), but not the ring map  → B̂ induced by a local homomorphism φ : A → B between local rings. This file builds it: the level-n components  → A/𝔪_Aⁿ → B/𝔪_Bⁿ (evaluation, then the quotient map of φ, which exists because φ(𝔪_A) ⊆ 𝔪_B) form a compatible family, and liftRingHom assembles them.

Properties: completionMap φ extends φ along the canonical maps (completionMap_of), its level-n evaluation is the quotient map of φ (evalₐ_completionMap), it is characterized by that (completionMap_unique), and it is local (isLocalHom_completionMap). It is used for the completed chart map (Hironaka/Algebra/Local/ChartCompletion.lean), for the transfer of orders through the completion (Hironaka/Algebra/Local/Lemma61.lean, ChartOrderFaithful.lean) and for the completion of the graph of an étale map (Hironaka/Scheme/Smooth/GraphCompletion.lean).

theorem IsLocalRing.factorPow_evalₐ {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hle : m ≤ n) (x : AdicCompletion I R) : (Ideal.Quotient.factorPow I hle) ((AdicCompletion.evalₐ I n) x) = (AdicCompletion.evalₐ I m) x

The evaluations of the completion at levels m ≤ n are compatible through the factor map R ⧸ Iⁿ → R ⧸ Iᵐ.

theorem IsLocalRing.maximalIdeal_pow_le_comap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] (n : ℕ) : maximalIdeal A ^ n ≤ Ideal.comap φ (maximalIdeal B ^ n)

noncomputable def IsLocalRing.completionMapLevel {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] (n : ℕ) : AdicCompletion (maximalIdeal A) A →+* B ⧸ maximalIdeal B ^ n

The level-n component of the induced map:  → A/𝔪_Aⁿ → B/𝔪_Bⁿ.

Equations

• IsLocalRing.completionMapLevel φ n = (Ideal.quotientMap (IsLocalRing.maximalIdeal B ^ n) φ ⋯).comp ↑(AdicCompletion.evalₐ (IsLocalRing.maximalIdeal A) n)

theorem IsLocalRing.completionMapLevel_compat {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] {m n : ℕ} (hle : m ≤ n) : (Ideal.Quotient.factorPow (maximalIdeal B) hle).comp (completionMapLevel φ n) = completionMapLevel φ m

noncomputable def IsLocalRing.completionMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] : AdicCompletion (maximalIdeal A) A →+* AdicCompletion (maximalIdeal B) B

The ring map  → B̂ induced on maximal-adic completions by the local homomorphism φ.

Equations

• IsLocalRing.completionMap φ = AdicCompletion.liftRingHom (IsLocalRing.maximalIdeal B) (IsLocalRing.completionMapLevel φ) ⋯

theorem IsLocalRing.evalₐ_completionMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] (n : ℕ) (x : AdicCompletion (maximalIdeal A) A) : (AdicCompletion.evalₐ (maximalIdeal B) n) ((completionMap φ) x) = (Ideal.quotientMap (maximalIdeal B ^ n) φ ⋯) ((AdicCompletion.evalₐ (maximalIdeal A) n) x)

theorem IsLocalRing.completionMap_of {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] (a : A) : (completionMap φ) ((AdicCompletion.of (maximalIdeal A) A) a) = (AdicCompletion.of (maximalIdeal B) B) (φ a)

The induced map extends φ:  → B̂ composed with A → Â is B → B̂ composed with φ.

theorem IsLocalRing.completionMap_algebraMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] (a : A) : (completionMap φ) ((algebraMap A (AdicCompletion (maximalIdeal A) A)) a) = (algebraMap B (AdicCompletion (maximalIdeal B) B)) (φ a)

theorem IsLocalRing.completionMap_unique {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) [IsLocalHom φ] (F : AdicCompletion (maximalIdeal A) A →+* AdicCompletion (maximalIdeal B) B) (hF : ∀ (n : ℕ) (x : AdicCompletion (maximalIdeal A) A), (AdicCompletion.evalₐ (maximalIdeal B) n) (F x) = (Ideal.quotientMap (maximalIdeal B ^ n) φ ⋯) ((AdicCompletion.evalₐ (maximalIdeal A) n) x)) : F = completionMap φ

Uniqueness: a ring map  → B̂ whose level-n evaluations are the quotient maps of φ is the induced map.

theorem IsLocalRing.map_maximalIdeal_pow_completionMap_le {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] (φ : A →+* B) [IsLocalHom φ] (k : ℕ) : Ideal.map (completionMap φ) (maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ k) ≤ maximalIdeal (AdicCompletion (maximalIdeal B) B) ^ k

The induced map sends 𝔪_Âᵏ into 𝔪_B̂ᵏ (𝔪_Â = 𝔪_A Â, 𝔪_B̂ = 𝔪_B B̂, and φ(𝔪_A) ⊆ 𝔪_B).

theorem IsLocalRing.completionMap_mem_maximalIdeal_pow {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] (φ : A →+* B) [IsLocalHom φ] {x : AdicCompletion (maximalIdeal A) A} {k : ℕ} (hx : x ∈ maximalIdeal (AdicCompletion (maximalIdeal A) A) ^ k) : (completionMap φ) x ∈ maximalIdeal (AdicCompletion (maximalIdeal B) B) ^ k

instance IsLocalRing.isLocalHom_completionMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] (φ : A →+* B) [IsLocalHom φ] : IsLocalHom (completionMap φ)

The induced map is a local homomorphism.

theorem IsLocalRing.ordElem_le_ordElem_completionMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] (φ : A →+* B) [IsLocalHom φ] (x : AdicCompletion (maximalIdeal A) A) : ordElem x ≤ ordElem ((completionMap φ) x)

Orders do not decrease along the induced map.

theorem IsLocalRing.completionMap_congr {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {φ ψ : A →+* B} [IsLocalHom φ] [IsLocalHom ψ] (h : φ = ψ) : completionMap φ = completionMap ψ

theorem IsLocalRing.completionMap_id {A : Type u_1} [CommRing A] [IsLocalRing A] : completionMap (RingHom.id A) = RingHom.id (AdicCompletion (maximalIdeal A) A)

theorem IsLocalRing.completionMap_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [IsLocalRing A] [IsLocalRing B] [IsLocalRing C] (φ : A →+* B) (ψ : B →+* C) [IsLocalHom φ] [IsLocalHom ψ] : completionMap (ψ.comp φ) = (completionMap ψ).comp (completionMap φ)

instance IsLocalRing.instIsLocalHomRingEquivToRingHom {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (e : A ≃+* B) : IsLocalHom ↑e

A ring isomorphism is a local homomorphism (instance form of isLocalHom_ringEquiv).

theorem IsLocalRing.completionMap_eq_id_of {A : Type u_1} [CommRing A] [IsLocalRing A] (φ : A →+* A) [IsLocalHom φ] (h : ∀ (a : A), φ a = a) : completionMap φ = RingHom.id (AdicCompletion (maximalIdeal A) A)

noncomputable def IsLocalRing.completionEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (e : A ≃+* B) : AdicCompletion (maximalIdeal A) A ≃+* AdicCompletion (maximalIdeal B) B

An isomorphism of local rings induces an isomorphism of their completions.

Equations

• IsLocalRing.completionEquiv e = RingEquiv.ofRingHom (IsLocalRing.completionMap ↑e) (IsLocalRing.completionMap ↑e.symm) ⋯ ⋯

theorem IsLocalRing.completionEquiv_apply {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (e : A ≃+* B) (x : AdicCompletion (maximalIdeal A) A) : (completionEquiv e) x = (completionMap ↑e) x

theorem IsLocalRing.residueField_map_completionMap_comp {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] (φ : A →+* B) [IsLocalHom φ] : (ResidueField.map (completionMap φ)).comp ↑(residueFieldEquiv A) = (↑(residueFieldEquiv B)).comp (ResidueField.map φ)

The induced map on completions is compatible with the identifications of residue fields (residueFieldEquiv): ResidueField.map φ̂ ∘ residueFieldEquiv A = residueFieldEquiv B ∘ ResidueField.map φ.

theorem IsLocalRing.residue_completionMap_coefficientField {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] (φ : A →+* B) [IsLocalHom φ] [Algebra ℚ A] (hbij : Function.Bijective ⇑(ResidueField.map φ)) (k : ResidueField B) : (residue (AdicCompletion (maximalIdeal B) B)) ((completionMap φ) ((coefficientField A) ((RingEquiv.ofBijective (ResidueField.map φ) hbij).symm k))) = (residueFieldEquiv B) k

For the coefficient field on B̂ transported from A along the induced map (ι_B := completionMap φ ∘ coefficientField A ∘ e⁻¹, e the induced isomorphism of residue fields when ResidueField.map φ is bijective), the section property IsCoefficientAlgebra holds.