Adic completions along algebra homomorphisms

Mathlib's AdicCompletion.map is functorial in the module for a fixed ring and ideal. This file makes the completion of a ring functorial in the pair (S, I): an R-algebra homomorphism f : S →ₐ[R] S' with I ≤ f⁻¹ I' induces an R-algebra homomorphism of completions AdicCompletion I S →ₐ[R] AdicCompletion I' S', and an R-algebra isomorphism carrying I onto I' induces an isomorphism of completions. This is what is needed to compare the completions of isomorphic local rings, for instance of two models of the localization of a ring at a prime.

Main definitions and results

• AdicCompletion.factor_evalₐ: the projections evalₐ I n are compatible with the transition maps S ⧸ I ^ n → S ⧸ I ^ m.
• AdicCompletion.mapₐ: the map of completions induced by an algebra homomorphism, with AdicCompletion.evalₐ_mapₐ and AdicCompletion.mapₐ_of, and the functoriality laws AdicCompletion.mapₐ_id and AdicCompletion.mapₐ_comp.
• AdicCompletion.mapₐ_injective and AdicCompletion.mapₐ_bijective: the map of completions is injective, resp. bijective, when all the maps S ⧸ I ^ n → S' ⧸ I' ^ n are. For instance a ring whose quotients by the powers of I agree with those of an I'-adically complete ring S' has completion S'.
• AdicCompletion.congrₐ: the isomorphism of completions induced by an algebra isomorphism, with AdicCompletion.toAlgHom_congrₐ (it is mapₐ of the underlying homomorphism), AdicCompletion.evalₐ_congrₐ, AdicCompletion.congrₐ_of, and the laws AdicCompletion.congrₐ_refl, AdicCompletion.congrₐ_symm and AdicCompletion.congrₐ_trans.

@[simp]

theorem AdicCompletion.factor_evalₐ {S : Type u_2} [CommRing S] {I : Ideal S} {m n : ℕ} (hle : m ≤ n) (x : AdicCompletion I S) : (Ideal.Quotient.factor ⋯) ((evalₐ I n) x) = (evalₐ I m) x

The projections of the adic completion to S ⧸ I ^ n are compatible with the transition maps S ⧸ I ^ n → S ⧸ I ^ m for m ≤ n.

noncomputable def AdicCompletion.mapₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') : AdicCompletion I S →ₐ[R] AdicCompletion I' S'

An R-algebra homomorphism f : S →ₐ[R] S' with I ≤ f⁻¹ I' induces an R-algebra homomorphism AdicCompletion I S →ₐ[R] AdicCompletion I' S', reducing modulo I' ^ n to the map S ⧸ I ^ n → S' ⧸ I' ^ n induced by f.

@[simp]

theorem AdicCompletion.evalₐ_mapₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') (n : ℕ) (x : AdicCompletion I S) : (evalₐ I' n) ((mapₐ f hf) x) = (Ideal.quotientMap (I' ^ n) f.toRingHom ⋯) ((evalₐ I n) x)

Modulo I' ^ n, the map of completions mapₐ f hf is the map S ⧸ I ^ n → S' ⧸ I' ^ n induced by f.

@[simp]

theorem AdicCompletion.mapₐ_of {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') (x : S) : (mapₐ f hf) ((of I S) x) = (of I' S') (f x)

The map of completions extends f along the canonical maps S → AdicCompletion I S and S' → AdicCompletion I' S'.

theorem AdicCompletion.mapₐ_injective {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') (h : ∀ (n : ℕ), Function.Injective ⇑(Ideal.quotientMap (I' ^ n) f.toRingHom ⋯)) : Function.Injective ⇑(mapₐ f hf)

The map of completions is injective if every map S ⧸ I ^ n → S' ⧸ I' ^ n induced by f is injective.

theorem AdicCompletion.mapₐ_bijective {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') (h : ∀ (n : ℕ), Function.Bijective ⇑(Ideal.quotientMap (I' ^ n) f.toRingHom ⋯)) : Function.Bijective ⇑(mapₐ f hf)

Completions agree when all the quotients do. The map of completions is bijective if every map S ⧸ I ^ n → S' ⧸ I' ^ n induced by f is bijective.

@[simp]

theorem AdicCompletion.mapₐ_id {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal S} (hf : I ≤ Ideal.comap (AlgHom.id R S) I) : mapₐ (AlgHom.id R S) hf = AlgHom.id R (AdicCompletion I S)

The identity of S induces the identity of AdicCompletion I S.

theorem AdicCompletion.mapₐ_comp {R : Type u_1} {S : Type u_2} {S' : Type u_3} {S'' : Type u_4} [CommRing R] [CommRing S] [CommRing S'] [CommRing S''] [Algebra R S] [Algebra R S'] [Algebra R S''] {I : Ideal S} {I' : Ideal S'} {I'' : Ideal S''} (g : S' →ₐ[R] S'') (hg : I' ≤ Ideal.comap g I'') (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') : (mapₐ g hg).comp (mapₐ f hf) = mapₐ (g.comp f) ⋯

The map of completions induced by a composite is the composite of the induced maps.

@[simp]

theorem AdicCompletion.mapₐ_mapₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} {S'' : Type u_4} [CommRing R] [CommRing S] [CommRing S'] [CommRing S''] [Algebra R S] [Algebra R S'] [Algebra R S''] {I : Ideal S} {I' : Ideal S'} {I'' : Ideal S''} (g : S' →ₐ[R] S'') (hg : I' ≤ Ideal.comap g I'') (f : S →ₐ[R] S') (hf : I ≤ Ideal.comap f I') (x : AdicCompletion I S) : (mapₐ g hg) ((mapₐ f hf) x) = (mapₐ (g.comp f) ⋯) x

Pointwise form of AdicCompletion.mapₐ_comp.

noncomputable def AdicCompletion.congrₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') : AdicCompletion I S ≃ₐ[R] AdicCompletion I' S'

An R-algebra isomorphism e : S ≃ₐ[R] S' carrying I onto I' induces an R-algebra isomorphism AdicCompletion I S ≃ₐ[R] AdicCompletion I' S'.

@[simp]

theorem AdicCompletion.toAlgHom_congrₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') : ↑(congrₐ e he) = mapₐ ↑e ⋯

As an algebra homomorphism, congrₐ e he is the map of completions induced by e.

@[simp]

theorem AdicCompletion.congrₐ_refl {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal S} (he : Ideal.map AlgEquiv.refl I = I) : congrₐ AlgEquiv.refl he = AlgEquiv.refl

The identity isomorphism of S induces the identity isomorphism of AdicCompletion I S.

@[simp]

theorem AdicCompletion.congrₐ_symm {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') : (congrₐ e he).symm = congrₐ e.symm ⋯

The inverse of congrₐ e he is the isomorphism of completions induced by e.symm.

@[simp]

theorem AdicCompletion.congrₐ_trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} {S'' : Type u_4} [CommRing R] [CommRing S] [CommRing S'] [CommRing S''] [Algebra R S] [Algebra R S'] [Algebra R S''] {I : Ideal S} {I' : Ideal S'} {I'' : Ideal S''} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') (e' : S' ≃ₐ[R] S'') (he' : Ideal.map e' I' = I'') : (congrₐ e he).trans (congrₐ e' he') = congrₐ (e.trans e') ⋯

The isomorphism of completions induced by a composite is the composite of the induced isomorphisms.

@[simp]

theorem AdicCompletion.congrₐ_congrₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} {S'' : Type u_4} [CommRing R] [CommRing S] [CommRing S'] [CommRing S''] [Algebra R S] [Algebra R S'] [Algebra R S''] {I : Ideal S} {I' : Ideal S'} {I'' : Ideal S''} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') (e' : S' ≃ₐ[R] S'') (he' : Ideal.map e' I' = I'') (x : AdicCompletion I S) : (congrₐ e' he') ((congrₐ e he) x) = (congrₐ (e.trans e') ⋯) x

Pointwise form of AdicCompletion.congrₐ_trans.

@[simp]

theorem AdicCompletion.congrₐ_of {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') (x : S) : (congrₐ e he) ((of I S) x) = (of I' S') (e x)

The isomorphism of completions extends e along the canonical maps into the completions.

@[simp]

theorem AdicCompletion.evalₐ_congrₐ {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') (n : ℕ) (x : AdicCompletion I S) : (evalₐ I' n) ((congrₐ e he) x) = (Ideal.quotientMap (I' ^ n) ↑e ⋯) ((evalₐ I n) x)

Modulo I' ^ n, the isomorphism of completions congrₐ e he is the map S ⧸ I ^ n → S' ⧸ I' ^ n induced by e.

theorem AdicCompletion.evalₐ_congrₐ_symm {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') (n : ℕ) (x : AdicCompletion I' S') : (evalₐ I n) ((congrₐ e he).symm x) = (Ideal.quotientMap (I ^ n) ↑e.symm ⋯) ((evalₐ I' n) x)

Modulo I ^ n, the inverse of congrₐ e he is the map S' ⧸ I' ^ n → S ⧸ I ^ n induced by e.symm.

theorem AdicCompletion.congrₐ_symm_of {R : Type u_1} {S : Type u_2} {S' : Type u_3} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] {I : Ideal S} {I' : Ideal S'} (e : S ≃ₐ[R] S') (he : Ideal.map e I = I') (x : S') : (congrₐ e he).symm ((of I' S') x) = (of I S) (e.symm x)

The inverse of congrₐ e he extends e.symm along the canonical maps into the completions.