# Documentation

Mathlib.RingTheory.Localization.AtPrime

# 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 : ] :

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

Instances For
theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [] (P : ) [hp : ] [] :
@[inline, reducible]
abbrev IsLocalization.AtPrime {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (P : ) [hp : ] :

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.

Instances For
@[inline, reducible]
abbrev Localization.AtPrime {R : Type u_1} [] (P : ) [hp : ] :
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.

Instances For
theorem IsLocalization.AtPrime.Nontrivial {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (P : ) [hp : ] [] :
theorem IsLocalization.AtPrime.localRing {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (P : ) [hp : ] [] :
instance Localization.AtPrime.localRing {R : Type u_1} [] (P : ) [hp : ] :

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

instance IsLocalization.isDomain_of_local_atPrime {A : Type u_4} [] [] {P : } :
∀ (x : ),

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

theorem IsLocalization.AtPrime.isUnit_to_map_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : ] [] (x : R) :
IsUnit (↑() x)
theorem IsLocalization.AtPrime.to_map_mem_maximal_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : ] [] (x : R) (h : optParam () (_ : )) :
↑() x x I
theorem IsLocalization.AtPrime.comap_maximalIdeal {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : ] [] (h : optParam () (_ : )) :
Ideal.comap () () = I
theorem IsLocalization.AtPrime.isUnit_mk'_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : ] [] (x : R) (y : { x // }) :
theorem IsLocalization.AtPrime.mk'_mem_maximal_iff {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) [hI : ] [] (x : R) (y : { x // }) (h : optParam () (_ : )) :
x I
theorem Localization.AtPrime.comap_maximalIdeal {R : Type u_1} [] {I : } [hI : ] :

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 : ] :

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 : ] {J : } [hJ : ] {f : R →+* P} :
I
noncomputable def Localization.localRingHom {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : ] (J : ) [] (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.

Instances For
theorem Localization.localRingHom_to_map {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : ] (J : ) [] (f : R →+* P) (hIJ : I = ) (x : R) :
↑() (↑() x) = ↑(algebraMap ((fun x => P) x) ()) (f x)
theorem Localization.localRingHom_mk' {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : ] (J : ) [] (f : R →+* P) (hIJ : I = ) (x : R) (y : { x // }) :
↑() () = IsLocalization.mk' () (f x) { val := f y, property := (_ : y ) }
instance Localization.isLocalRingHom_localRingHom {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : ] (J : ) [hJ : ] (f : R →+* P) (hIJ : I = ) :
theorem Localization.localRingHom_unique {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : ] (J : ) [] (f : R →+* P) (hIJ : I = ) {j : } (hj : ∀ (x : R), j (↑() x) = ↑(algebraMap ((fun x => P) x) ()) (f x)) :
= j
@[simp]
theorem Localization.localRingHom_id {R : Type u_1} [] (I : ) [hI : ] :
Localization.localRingHom I I () (_ : I = ) =
theorem Localization.localRingHom_comp {R : Type u_1} [] {P : Type u_3} [] (I : ) [hI : ] {S : Type u_4} [] (J : ) [hJ : ] (K : ) [hK : ] (f : R →+* S) (hIJ : I = ) (g : S →+* P) (hJK : J = ) :