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, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) ↑x.fst

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