# mathlibdocumentation

ring_theory.localization.at_prime

# Localizations of commutative rings at the complement of a prime ideal #

## Main definitions #

• is_localization.at_prime (I : ideal R) [is_prime I] (S : Type*) expresses that S is a localization at (the complement of) a prime ideal I, as an abbreviation of is_localization I.prime_compl S

## Main results #

• is_localization.at_prime.local_ring: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring

## Implementation notes #

See src/ring_theory/localization/basic.lean for a design overview.

## Tags #

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

def ideal.prime_compl {R : Type u_1} (I : ideal R) [hp : I.is_prime] :

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

Equations
Instances for ideal.prime_compl
@[protected]
def is_localization.at_prime {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hp : I.is_prime] :
Prop

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

@[protected]
def localization.at_prime {R : Type u_1} (I : ideal R) [hp : I.is_prime] :
Type u_1

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

theorem is_localization.at_prime.nontrivial {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hp : I.is_prime]  :
theorem is_localization.at_prime.local_ring {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hp : I.is_prime]  :
@[protected, instance]
def localization.at_prime.local_ring {R : Type u_1} (I : ideal R) [hp : I.is_prime] :

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

@[protected, instance]
def is_localization.is_domain_of_local_at_prime {A : Type u_4} [comm_ring A] [is_domain A] {P : ideal A} (hp : P.is_prime) :

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

theorem is_localization.at_prime.is_unit_to_map_iff {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hI : I.is_prime] (x : R) :
theorem is_localization.at_prime.to_map_mem_maximal_iff {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hI : I.is_prime] (x : R) (h : := _) :
S) x x I
theorem is_localization.at_prime.is_unit_mk'_iff {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hI : I.is_prime] (x : R) (y : (I.prime_compl)) :
theorem is_localization.at_prime.mk'_mem_maximal_iff {R : Type u_1} (S : Type u_2) [ S] (I : ideal R) [hI : I.is_prime] (x : R) (y : (I.prime_compl)) (h : := _) :
x I
theorem localization.at_prime.comap_maximal_ideal {R : Type u_1} {I : ideal R} [hI : I.is_prime] :

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

theorem localization.at_prime.map_eq_maximal_ideal {R : Type u_1} {I : ideal R} [hI : I.is_prime] :

The image of I in the localization at I.prime_compl is a maximal ideal, and in particular it is the unique maximal ideal given by the local ring structure at_prime.local_ring

theorem localization.le_comap_prime_compl_iff {R : Type u_1} {P : Type u_3} {I : ideal R} [hI : I.is_prime] {J : ideal P} [hJ : J.is_prime] {f : R →+* P} :
J I
noncomputable def localization.local_ring_hom {R : Type u_1} {P : Type u_3} (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = 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
• hIJ =
Instances for localization.local_ring_hom
theorem localization.local_ring_hom_to_map {R : Type u_1} {P : Type u_3} (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = J) (x : R) :
hIJ) ( x) = (f x)
theorem localization.local_ring_hom_mk' {R : Type u_1} {P : Type u_3} (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = J) (x : R) (y : (I.prime_compl)) :
hIJ) y) = f y, _⟩
@[protected, instance]
def localization.is_local_ring_hom_local_ring_hom {R : Type u_1} {P : Type u_3} (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = J) :
theorem localization.local_ring_hom_unique {R : Type u_1} {P : Type u_3} (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = J) (hj : ∀ (x : R), j ( x) = (f x)) :
hIJ = j
@[simp]
theorem localization.local_ring_hom_id {R : Type u_1} (I : ideal R) [hI : I.is_prime] :
@[simp]
theorem localization.local_ring_hom_comp {R : Type u_1} {P : Type u_3} (I : ideal R) [hI : I.is_prime] {S : Type u_2} (J : ideal S) [hJ : J.is_prime] (K : ideal P) [hK : K.is_prime] (f : R →+* S) (hIJ : I = J) (g : S →+* P) (hJK : J = K) :
(g.comp f) _ = hJK).comp hIJ)