# mathlib3documentation

ring_theory.localization.ideal

# Ideals in localizations of commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem is_localization.mem_map_algebra_map_iff {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] {I : ideal R} {z : S} :
z ideal.map S) I (x : I × M), z * S) (x.snd) = S) (x.fst)
theorem is_localization.map_comap {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (J : ideal S) :
ideal.map S) (ideal.comap S) J) = J
theorem is_localization.comap_map_of_is_prime_disjoint {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (I : ideal R) (hI : I.is_prime) (hM : I) :
ideal.comap S) (ideal.map S) I) = I
def is_localization.order_embedding {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :

If S is the localization of R at a submonoid, the ordering of ideals of S is embedded in the ordering of ideals of R.

Equations
theorem is_localization.is_prime_iff_is_prime_disjoint {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (J : ideal S) :

If R is a ring, then prime ideals in the localization at M correspond to prime ideals in the original ring R that are disjoint from M. This lemma gives the particular case for an ideal and its comap, see le_rel_iso_of_prime for the more general relation isomorphism

theorem is_localization.is_prime_of_is_prime_disjoint {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] (I : ideal R) (hp : I.is_prime) (hd : I) :

If R is a ring, then prime ideals in the localization at M correspond to prime ideals in the original ring R that are disjoint from M. This lemma gives the particular case for an ideal and its map, see le_rel_iso_of_prime for the more general relation isomorphism, and the reverse implication

def is_localization.order_iso_of_prime {R : Type u_1} (M : submonoid R) (S : Type u_2) [ S] [ S] :
{p // p.is_prime} ≃o {p // p.is_prime p}

If R is a ring, then prime ideals in the localization at M correspond to prime ideals in the original ring R that are disjoint from M

Equations
theorem is_localization.surjective_quotient_map_of_maximal_of_localization {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] {I : ideal S} [I.is_prime] {J : ideal R} {H : J ideal.comap S) I} (hI : (ideal.comap S) I).is_maximal) :

quotient_map applied to maximal ideals of a localization is surjective. The quotient by a maximal ideal is a field, so inverses to elements already exist, and the localization necessarily maps the equivalence class of the inverse in the localization

theorem is_localization.bot_lt_comap_prime {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] [is_domain R] (hM : M ) (p : ideal S) [hpp : p.is_prime] (hp0 : p ) :