Ideals in localizations of commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Implementation notes #

See src/ring_theory/localization/basic.lean for a design overview.

Tags #

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

source

theorem is_localization.mem_map_algebra_map_iff {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] {I : ideal R} {z : S} :

z ∈ ideal.map (algebra_map R S) I ↔ ∃ (x : ↥I × ↥M), z * ⇑(algebra_map R S) ↑(x.snd) = ⇑(algebra_map R S) ↑(x.fst)

source

theorem is_localization.map_comap {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (J : ideal S) :

ideal.map (algebra_map R S) (ideal.comap (algebra_map R S) J) = J

source

theorem is_localization.comap_map_of_is_prime_disjoint {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (I : ideal R) (hI : I.is_prime) (hM : disjoint ↑M ↑I) :

ideal.comap (algebra_map R S) (ideal.map (algebra_map R S) I) = I

source

def is_localization.order_embedding {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization 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

is_localization.order_embedding M S = {to_embedding := {to_fun := λ (J : ideal S), ideal.comap (algebra_map R S) J, inj' := _}, map_rel_iff' := _}

source

theorem is_localization.is_prime_iff_is_prime_disjoint {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (J : ideal S) :

J.is_prime ↔ (ideal.comap (algebra_map R S) J).is_prime ∧ disjoint ↑M ↑(ideal.comap (algebra_map 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 is_localization.is_prime_of_is_prime_disjoint {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (I : ideal R) (hp : I.is_prime) (hd : disjoint ↑M ↑I) :

(ideal.map (algebra_map R S) I).is_prime

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 is_localization.order_iso_of_prime {R : Type u_1} [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] :

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

is_localization.order_iso_of_prime M S = {to_equiv := {to_fun := λ (p : {p // p.is_prime}), ⟨ideal.comap (algebra_map R S) p.val, _⟩, inv_fun := λ (p : {p // p.is_prime ∧ disjoint ↑M ↑p}), ⟨ideal.map (algebra_map R S) p.val, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

theorem is_localization.surjective_quotient_map_of_maximal_of_localization {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] {I : ideal S} [I.is_prime] {J : ideal R} {H : J ≤ ideal.comap (algebra_map R S) I} (hI : (ideal.comap (algebra_map R S) I).is_maximal) :

function.surjective ⇑(I.quotient_map (algebra_map R S) H)

quotient_map 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 is_localization.bot_lt_comap_prime {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] [is_domain R] (hM : M ≤ non_zero_divisors R) (p : ideal S) [hpp : p.is_prime] (hp0 : p ≠ ⊥) :

⊥ < ideal.comap (algebra_map R S) p