mathlib3 documentation

ring_theory.localization.ideal

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

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

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

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

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

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

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

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

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