Localizations of commutative rings at the complement of a prime ideal

Main definitions

• IsLocalization.AtPrime (P : Ideal R) [IsPrime P] (S : Type*) expresses that S is a localization at (the complement of) a prime ideal P, as an abbreviation of IsLocalization P.prime_compl S

Main results

• IsLocalization.AtPrime.isLocalRing: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring

Implementation notes

See RingTheory.Localization.Basic for a design overview.

Tags

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

def Ideal.primeCompl {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] : Submonoid R

The complement of a prime ideal P ⊆ R is a submonoid of R.

Equations

• P.primeCompl = { carrier := (↑P)ᶜ, mul_mem' := ⋯, one_mem' := ⋯ }

theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] [NoZeroDivisors R] : P.primeCompl ≤ nonZeroDivisors R

@[reducible, inline]

abbrev IsLocalization.AtPrime {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] : Prop

Given a prime ideal P, the typeclass IsLocalization.AtPrime S P states that S is isomorphic to the localization of R at the complement of P.

Equations

• IsLocalization.AtPrime S P = IsLocalization P.primeCompl S

@[reducible, inline]

abbrev Localization.AtPrime {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] : Type u_1

Given a prime ideal P, Localization.AtPrime P is a localization of R at the complement of P, as a quotient type.

Equations

• Localization.AtPrime P = Localization P.primeCompl

theorem IsLocalization.AtPrime.Nontrivial {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : Nontrivial S

theorem IsLocalization.AtPrime.isLocalRing {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : IsLocalRing S

@[deprecated IsLocalization.AtPrime.isLocalRing]

theorem IsLocalization.AtPrime.localRing {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : IsLocalRing S

Alias of IsLocalization.AtPrime.isLocalRing.

instance Localization.AtPrime.isLocalRing {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] : IsLocalRing (Localization P.primeCompl)

The localization of R at the complement of a prime ideal is a local ring.

Equations

• ⋯ = ⋯

instance IsLocalization.isDomain_of_local_atPrime {A : Type u_4} [CommRing A] [IsDomain A] {P : Ideal A} (x✝ : P.IsPrime) : IsDomain (Localization.AtPrime P)

The localization of an integral domain at the complement of a prime ideal is an integral domain.

Equations

• ⋯ = ⋯

def IsLocalization.AtPrime.orderIsoOfPrime {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] : { p : Ideal S // p.IsPrime } ≃o { p : Ideal R // p.IsPrime ∧ p ≤ I }

The prime ideals in the localization of a commutative ring at a prime ideal I are in order-preserving bijection with the prime ideals contained in I.

Equations

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

theorem IsLocalization.AtPrime.isUnit_to_map_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) : IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl

theorem IsLocalization.AtPrime.to_map_mem_maximal_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (h : IsLocalRing S := ⋯) : (algebraMap R S) x ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I

theorem IsLocalization.AtPrime.comap_maximalIdeal {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (h : IsLocalRing S := ⋯) : Ideal.comap (algebraMap R S) (IsLocalRing.maximalIdeal S) = I

theorem IsLocalization.AtPrime.isUnit_mk'_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) : IsUnit (IsLocalization.mk' S x y) ↔ x ∈ I.primeCompl

theorem IsLocalization.AtPrime.mk'_mem_maximal_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) (h : IsLocalRing S := ⋯) : IsLocalization.mk' S x y ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I

theorem Localization.AtPrime.comap_maximalIdeal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] : Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I

The unique maximal ideal of the localization at I.primeCompl lies over the ideal I.

theorem Localization.AtPrime.map_eq_maximalIdeal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] : Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)

The image of I in the localization at I.primeCompl is a maximal ideal, and in particular it is the unique maximal ideal given by the local ring structure AtPrime.isLocalRing

theorem Localization.le_comap_primeCompl_iff {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] {I : Ideal R} [hI : I.IsPrime] {J : Ideal P} [J.IsPrime] {f : R →+* P} : I.primeCompl ≤ Submonoid.comap f J.primeCompl ↔ Ideal.comap f J ≤ I

noncomputable def Localization.localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) : Localization.AtPrime I →+* Localization.AtPrime J

For a ring hom f : R →+* S and a prime ideal J in S, the induced ring hom from the localization of R at J.comap f to the localization of S at J.

To make this definition more flexible, we allow any ideal I of R as input, together with a proof that I = J.comap f. This can be useful when I is not definitionally equal to J.comap f.

Equations

• Localization.localRingHom I J f hIJ = IsLocalization.map (Localization.AtPrime J) f ⋯

theorem Localization.localRingHom_to_map {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) : (Localization.localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)

theorem Localization.localRingHom_mk' {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) (y : ↥I.primeCompl) : (Localization.localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩

theorem Localization.isLocalHom_localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) : IsLocalHom (Localization.localRingHom I J f hIJ)

@[deprecated Localization.isLocalHom_localRingHom]

theorem Localization.isLocalRingHom_localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) : IsLocalHom (Localization.localRingHom I J f hIJ)

Alias of Localization.isLocalHom_localRingHom.

theorem Localization.localRingHom_unique {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) {j : Localization.AtPrime I →+* Localization.AtPrime J} (hj : ∀ (x : R), j ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)) : Localization.localRingHom I J f hIJ = j

@[simp]

theorem Localization.localRingHom_id {R : Type u_1} [CommSemiring R] (I : Ideal R) [hI : I.IsPrime] : Localization.localRingHom I I (RingHom.id R) ⋯ = RingHom.id (Localization.AtPrime I)

theorem Localization.localRingHom_comp {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] {S : Type u_4} [CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P) [hK : K.IsPrime] (f : R →+* S) (hIJ : I = Ideal.comap f J) (g : S →+* P) (hJK : J = Ideal.comap g K) : Localization.localRingHom I K (g.comp f) ⋯ = (Localization.localRingHom J K g hJK).comp (Localization.localRingHom I J f hIJ)

def RingHom.toLocalizationIsMaximal (R : Type u_1) [CommSemiring R] : R →+* (I : { I : Ideal R // I.IsMaximal }) → Localization.AtPrime ↑I

The canonical ring homomorphism from a commutative semiring to the product of its localizations at all maximal ideals. It is always injective.

Equations

• RingHom.toLocalizationIsMaximal R = Pi.ringHom fun (x : { I : Ideal R // I.IsMaximal }) => algebraMap R (Localization.AtPrime ↑x)

theorem RingHom.toLocalizationIsMaximal_injective (R : Type u_1) [CommSemiring R] : Function.Injective ⇑(RingHom.toLocalizationIsMaximal R)