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.mk'_mem_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : ↥M} {I : Ideal S} :
mk' S x y ∈ I ↔ (algebraMap R S) x ∈ I
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.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) :
mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I
source
theorem IsLocalization.algebraMap_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) :
(algebraMap R S) x ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I
source
theorem IsLocalization.map_algebraMap_ne_top_iff_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) :
Ideal.map (algebraMap R S) I ≠ ⊤ ↔ Disjoint ↑M ↑I
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 : I.IsPrime) (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
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) :
    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

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

    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 // 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
      source
      theorem IsLocalization.map_radical {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) :
      Ideal.map (algebraMap R S) I.radical = (Ideal.map (algebraMap R S) I).radical
      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} [I.IsPrime] {J : Ideal R} {H : J ≤ Ideal.comap (algebraMap R S) I} (hI : (Ideal.comap (algebraMap R S) I).IsMaximal) :
      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 : p.IsPrime] (hp0 : p ≠ ⊥) :
      ⊥ < Ideal.comap (algebraMap R S) p
      source
      theorem IsLocalization.ideal_eq_iInf_comap_map_away {R : Type u_1} [CommRing R] {S : Finset R} (hS : Ideal.span ↑S = ⊤) (I : Ideal R) :
      I = ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
      source
      theorem NoZeroSMulDivisors_of_isLocalization (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (Rₚ : Type u_3) (Sₚ : Type u_4) [CommRing Rₚ] [CommRing Sₚ] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] {M : Submonoid R} (hM : M ≤ nonZeroDivisors R) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [NoZeroSMulDivisors R S] [IsDomain S] :
      NoZeroSMulDivisors Rₚ Sₚ
      source
      theorem IsLocalization.of_surjective {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {R' : Type u_3} {S' : Type u_4} [CommRing R'] [CommRing S'] [Algebra R' S'] (f : R →+* R') (hf : Function.Surjective ⇑f) (g : S →+* S') (hg : Function.Surjective ⇑g) (H : g.comp (algebraMap R S) = (algebraMap R' S').comp f) (H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)) :
      IsLocalization (Submonoid.map f M) S'