# 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.localRing: 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} [] (P : ) [hp : P.IsPrime] :

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

Equations
• P.primeCompl = { carrier := (↑P), mul_mem' := , one_mem' := }
Instances For
theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [] (P : ) [hp : P.IsPrime] [] :
P.primeCompl
@[reducible, inline]
abbrev IsLocalization.AtPrime {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (P : ) [hp : P.IsPrime] :

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
Instances For
@[reducible, inline]
abbrev Localization.AtPrime {R : Type u_1} [] (P : ) [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
Instances For
theorem IsLocalization.AtPrime.Nontrivial {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (P : ) [hp : P.IsPrime] [] :
theorem IsLocalization.AtPrime.localRing {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (P : ) [hp : P.IsPrime] [] :
instance Localization.AtPrime.localRing {R : Type u_1} [] (P : ) [hp : P.IsPrime] :
LocalRing (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} [] [] {P : } :
∀ (x : P.IsPrime),

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} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : I.IsPrime] [] :
{ p : // p.IsPrime } ≃o { p : // 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.
Instances For
theorem IsLocalization.AtPrime.isUnit_to_map_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : I.IsPrime] [] (x : R) :
IsUnit ((algebraMap R S) x) x I.primeCompl
theorem IsLocalization.AtPrime.to_map_mem_maximal_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : I.IsPrime] [] (x : R) (h : optParam (LocalRing S) ) :
(algebraMap R S) x x I
theorem IsLocalization.AtPrime.comap_maximalIdeal {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : I.IsPrime] [] (h : optParam (LocalRing S) ) :
= I
theorem IsLocalization.AtPrime.isUnit_mk'_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : I.IsPrime] [] (x : R) (y : { x : R // x I.primeCompl }) :
IsUnit (IsLocalization.mk' S x y) x I.primeCompl
theorem IsLocalization.AtPrime.mk'_mem_maximal_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : I.IsPrime] [] (x : R) (y : { x : R // x I.primeCompl }) (h : optParam (LocalRing S) ) :
x I
theorem Localization.AtPrime.comap_maximalIdeal {R : Type u_1} [] {I : } [hI : I.IsPrime] :

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} [] {I : } [hI : I.IsPrime] :

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.localRing

theorem Localization.le_comap_primeCompl_iff {R : Type u_1} [] {P : Type u_3} [] {I : } [hI : I.IsPrime] {J : } [hJ : J.IsPrime] {f : R →+* P} :
I.primeCompl Submonoid.comap f J.primeCompl I
noncomputable def Localization.localRingHom {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : I.IsPrime] (J : ) [J.IsPrime] (f : R →+* P) (hIJ : I = ) :

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
Instances For
theorem Localization.localRingHom_to_map {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : I.IsPrime] (J : ) [J.IsPrime] (f : R →+* P) (hIJ : I = ) (x : R) :
(Localization.localRingHom I J f hIJ) ( x) = (f x)
theorem Localization.localRingHom_mk' {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : I.IsPrime] (J : ) [J.IsPrime] (f : R →+* P) (hIJ : I = ) (x : R) (y : { x : R // x I.primeCompl }) :
(Localization.localRingHom I J f hIJ) = IsLocalization.mk' (f x) f y,
instance Localization.isLocalRingHom_localRingHom {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : I.IsPrime] (J : ) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = ) :
Equations
• =
theorem Localization.localRingHom_unique {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : I.IsPrime] (J : ) [J.IsPrime] (f : R →+* P) (hIJ : I = ) {j : } (hj : ∀ (x : R), j ( x) = (f x)) :
= j
@[simp]
theorem Localization.localRingHom_id {R : Type u_1} [] (I : ) [hI : I.IsPrime] :
theorem Localization.localRingHom_comp {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : I.IsPrime] {S : Type u_4} [] (J : ) [hJ : J.IsPrime] (K : ) [hK : K.IsPrime] (f : R →+* S) (hIJ : I = ) (g : S →+* P) (hJK : J = ) :
Localization.localRingHom I K (g.comp f) = (Localization.localRingHom J K g hJK).comp (Localization.localRingHom I J f hIJ)