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

source
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
source
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) :
Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J) = J
source
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 : Ideal.IsPrime I) (hM : Disjoint ↑M ↑I) :
Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I
source
def IsLocalization.orderEmbedding {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] :
Ideal S ↪o Ideal R

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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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) :
    Ideal.IsPrime J ↔ Ideal.IsPrime (Ideal.comap (algebraMap R S) J) ∧ 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

    source
    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 : Ideal.IsPrime I) (hd : Disjoint ↑M ↑I) :
    Ideal.IsPrime (Ideal.map (algebraMap R S) 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

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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} [Ideal.IsPrime I] {J : Ideal R} {H : J ≤ Ideal.comap (algebraMap R S) I} (hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)) :
      Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)

      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

      source
      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 : Ideal.IsPrime p] (hp0 : p ≠ ⊥) :
      ⊥ < Ideal.comap (algebraMap R S) p