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} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {I : Ideal R} {z : S} :
z Ideal.map (algebraMap R S) I ∃ (x : I × M), z * (algebraMap R S) x.2 = (algebraMap R S) x.1
theorem IsLocalization.mk'_mem_map_algebraMap_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (x : R) (s : M) :
IsLocalization.mk' S x s Ideal.map (algebraMap R S) I sM, s * x I
theorem IsLocalization.map_comap {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (J : Ideal S) :
theorem IsLocalization.comap_map_of_isPrime_disjoint {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (hI : I.IsPrime) (hM : Disjoint M I) :

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
Instances For
    theorem IsLocalization.isPrime_iff_isPrime_disjoint {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (J : Ideal S) :
    J.IsPrime (Ideal.comap (algebraMap R S) J).IsPrime Disjoint M (Ideal.comap (algebraMap 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} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (hp : I.IsPrime) (hd : Disjoint M I) :
    (Ideal.map (algebraMap R S) 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} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] :
    { p : Ideal S // p.IsPrime } ≃o { p : Ideal R // 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} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {I : Ideal S} [I.IsPrime] {J : Ideal R} {H : J Ideal.comap (algebraMap R S) I} (hI : (Ideal.comap (algebraMap R S) 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} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] [IsDomain R] (hM : M nonZeroDivisors R) (p : Ideal S) [hpp : p.IsPrime] (hp0 : p ) :