Documentation

Mathlib.RingTheory.Localization.Ideal

Ideals in localizations of commutative rings #

Implementation notes #

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

TODO #

Restate the file in terms of Ideal.under.

Tags #

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

source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
theorem IsLocalization.map_inf {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I J : Ideal R) :
Ideal.map (algebraMap R S) (I โŠ“ J) = Ideal.map (algebraMap R S) I โŠ“ Ideal.map (algebraMap R S) J
source
๐Ÿ”ธ coverage
def IsLocalization.mapFrameHom {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] :
FrameHom (Ideal R) (Ideal S)

IsLocalization.map_inf as an FrameHom.

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem IsLocalization.mapFrameHom_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) :
    (mapFrameHom M S) I = Ideal.map (algebraMap R S) I
    source
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    theorem IsLocalization.comap_map_of_isPrimary_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.IsPrimary) (hM : Disjoint โ†‘M โ†‘I) :
    Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I
    source
    ๐Ÿ“ coverage
    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
    ๐Ÿ”ธ coverage
    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.

    Instances For
      source
      ๐Ÿ“ coverage
      theorem IsLocalization.comap_le_comap_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {I J : Ideal S} :
      Ideal.comap (algebraMap R S) I โ‰ค Ideal.comap (algebraMap R S) J โ†” I โ‰ค J
      source
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      theorem IsLocalization.disjoint_comap_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (J : Ideal S) :
      Disjoint โ†‘M โ†‘(Ideal.comap (algebraMap R S) J) โ†” J โ‰  โŠค
      source
      ๐Ÿ”ธ coverage
      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

      Instances For
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem IsLocalization.orderIsoOfPrime_symm_apply_coe {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (p : { p : Ideal R // p.IsPrime โˆง Disjoint โ†‘M โ†‘p }) :
        โ†‘((RelIso.symm (orderIsoOfPrime M S)) p) = Ideal.map (algebraMap R S) โ†‘p
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem IsLocalization.orderIsoOfPrime_apply_coe {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (p : { p : Ideal S // p.IsPrime }) :
        โ†‘((orderIsoOfPrime M S) p) = Ideal.comap (algebraMap R S) โ†‘p
        source
        ๐Ÿ”ธ coverage
        def IsLocalization.primeSpectrumOrderIso {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] :
        PrimeSpectrum S โ‰ƒo { p : PrimeSpectrum R // Disjoint โ†‘M โ†‘p.asIdeal }

        The prime spectrum of the localization of a ring at a submonoid M are in order-preserving bijection with subset of the prime spectrum of the ring consisting of prime ideals disjoint from M.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (aโœ : PrimeSpectrum S) :
          โ†‘(โ†‘((primeSpectrumOrderIso M S) aโœ)).asIdeal = โ‡‘(algebraMap R S) โปยน' โ†‘aโœ.asIdeal
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (aโœ : { p : PrimeSpectrum R // Disjoint โ†‘M โ†‘p.asIdeal }) :
          โ†‘((RelIso.symm (primeSpectrumOrderIso M S)) aโœ).asIdeal = โ‹‚ (s : Submodule S S), โ‹‚ (_ : โ†‘(โ†‘aโœ).asIdeal โŠ† โ‡‘(algebraMap R S) โปยน' โ†‘s), โ†‘s
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          theorem IsLocalization.ideal_eq_iInf_comap_map_away {R : Type u_1} [CommSemiring 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
          ๐Ÿ“ coverage
          theorem IsLocalization.map_eq_top_of_not_subset {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {I : Ideal R} (hle : ยฌโ†‘I โŠ† (โ†‘M)แถœ) :
          Ideal.map (algebraMap R S) I = โŠค
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          theorem Module.IsTorsionFree.of_isLocalization (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] {Rโ‚š : Type u_3} {Sโ‚š : Type u_4} [CommRing Rโ‚š] [IsDomain 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โ‚š] [IsTorsionFree R S] :
          IsTorsionFree Rโ‚š Sโ‚š
          source
          ๐Ÿ“ coverage
          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'
          source
          ๐Ÿ“ coverage
          instance IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {P : Ideal R} [P.IsPrime] [IsDomain R] [IsDomain S] [FaithfulSMul R S] :
          IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))