Localization at the maximal ideal of a local ring and at its preimages, and local lifts

Every element of a local ring S outside its maximal ideal is a unit, so the localization of S at its maximal ideal inverts only units and is S itself (Mathlib IsLocalization.atUnits). This file names that equivalence, as an isomorphism of R-algebras for any R-algebra structure on S, so that statements about Localization.AtPrime (maximalIdeal S) transfer to S along a single map.

More generally, a ring homomorphism f : A →+* R to a local ring extends to the localization of A at the preimage f⁻¹(𝔪_R), and this extension maps the maximal ideal into 𝔪_R. Hence an element whose image under f lies outside 𝔪_Rⁿ stays outside the n-th power of the maximal ideal of that localization. For f the constant coefficient map of a polynomial ring over R, this says that a polynomial whose constant coefficient lies outside 𝔪_R² does not lie in the square of the maximal ideal of the polynomial ring localized at (𝔪_R, X_i).

A homomorphism ψ : R →+* T to a local ring which inverts the complement of a prime p and maps p into the maximal ideal lifts to a local homomorphism from the localization of R at p. For instance, a homomorphism to a field factors locally through the localization at its kernel.

Main results

• IsLocalRing.algEquivLocalizationAtMaximalIdeal R S: the R-algebra isomorphism from a local ring S to its localization at its maximal ideal.
• IsLocalization.AtPrime.isLocalHom_lift: the lift of a homomorphism to a local ring along the localization at a prime mapped into the maximal ideal is local.
• TauCeti.algebraMap_notMem_maximalIdeal_pow: an element whose image under f : A →+* R is not in 𝔪_Rⁿ does not lie in the n-th power of the maximal ideal of A localized at f⁻¹(𝔪_R).

noncomputable def IsLocalRing.algEquivLocalizationAtMaximalIdeal (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] [IsLocalRing S] : S ≃ₐ[R] Localization.AtPrime (maximalIdeal S)

A local R-algebra S is isomorphic, as an R-algebra, to its localization at its maximal ideal: that localization inverts only units.

@[simp]

theorem IsLocalRing.algEquivLocalizationAtMaximalIdeal_apply (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] [IsLocalRing S] (s : S) : (algEquivLocalizationAtMaximalIdeal R S) s = (algebraMap S (Localization.AtPrime (maximalIdeal S))) s

The local-ring equivalence maps an element to its image in the localization.

theorem IsLocalization.AtPrime.isLocalHom_lift {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [IsLocalRing T] (p : Ideal R) [p.IsPrime] [IsLocalization.AtPrime S p] {ψ : R →+* T} (hψ : ∀ (y : ↥p.primeCompl), IsUnit (ψ ↑y)) (hp : p ≤ Ideal.comap ψ (IsLocalRing.maximalIdeal T)) : IsLocalHom (lift hψ)

Let ψ : R →+* T be a homomorphism to a local ring which inverts the complement of a prime p and maps p into the maximal ideal. Its lift to the localization S of R at p is a local homomorphism. For T a field, p can be the kernel of ψ.

theorem TauCeti.algebraMap_notMem_maximalIdeal_pow {A : Type u_1} {R : Type u_2} [CommSemiring A] [CommSemiring R] [IsLocalRing R] {f : A →+* R} {n : ℕ} {a : A} (ha : f a ∉ IsLocalRing.maximalIdeal R ^ n) : (algebraMap A (Localization.AtPrime (Ideal.comap f (IsLocalRing.maximalIdeal R)))) a ∉ IsLocalRing.maximalIdeal (Localization.AtPrime (Ideal.comap f (IsLocalRing.maximalIdeal R))) ^ n

Let f : A →+* R be a ring homomorphism to a local ring. An element of A whose image under f is not in 𝔪_Rⁿ does not lie in the n-th power of the maximal ideal of the localization of A at f⁻¹(𝔪_R): f extends to that localization, mapping its maximal ideal into 𝔪_R.