# Documentation

Mathlib.RingTheory.Localization.Ideal

# Ideals in localizations of commutative rings #

## Implementation notes #

See Mathlib/RingTheory/Localization/Basic.lean for a design overview.

## Tags #

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

theorem IsLocalization.mem_map_algebraMap_iff {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] {I : } {z : S} :
z Ideal.map () I x, z * ↑() x.snd = ↑() x.fst
theorem IsLocalization.map_comap {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (J : ) :
Ideal.map () (Ideal.comap () J) = J
theorem IsLocalization.comap_map_of_isPrime_disjoint {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (I : ) (hI : ) (hM : Disjoint M I) :
Ideal.comap () (Ideal.map () I) = I
def IsLocalization.orderEmbedding {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R 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.

Instances For
theorem IsLocalization.isPrime_iff_isPrime_disjoint {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (J : ) :

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 IsLocalization.isPrime_of_isPrime_disjoint {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (I : ) (hp : ) (hd : Disjoint M 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 IsLocalization.orderIsoOfPrime {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
{ p // } ≃o { p // Disjoint M 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

Instances For
theorem IsLocalization.surjective_quotientMap_of_maximal_of_localization {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] {I : } [] {J : } {H : J Ideal.comap () I} (hI : Ideal.IsMaximal (Ideal.comap () I)) :

quotientMap 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 IsLocalization.bot_lt_comap_prime {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] [] (hM : ) (p : ) [hpp : ] (hp0 : p ) :