# 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 : I × M), z * () x.2 = () x.1
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 : I.IsPrime) (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.

Equations
• = { toFun := fun (J : ) => Ideal.comap () J, inj' := , map_rel_iff' := }
Instances For
theorem IsLocalization.isPrime_iff_isPrime_disjoint {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (J : ) :
J.IsPrime (Ideal.comap () J).IsPrime Disjoint M (Ideal.comap () 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 : I.IsPrime) (hd : Disjoint M I) :
(Ideal.map () I).IsPrime

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 : // p.IsPrime } ≃o { p : // p.IsPrime 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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IsLocalization.surjective_quotientMap_of_maximal_of_localization {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] {I : } [I.IsPrime] {J : } {H : J Ideal.comap () I} (hI : (Ideal.comap () I).IsMaximal) :

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 : p.IsPrime] (hp0 : p ) :