mathlib documentation

ring_theory.localization.at_prime

Localizations of commutative rings at the complement of a prime ideal #

Main definitions #

Main results #

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

@[protected]
def is_localization.at_prime {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hp : I.is_prime] :
Prop

Given a prime ideal P, the typeclass is_localization.at_prime S P states that S is isomorphic to the localization of R at the complement of P.

@[protected]
def localization.at_prime {R : Type u_1} [comm_semiring R] (I : ideal R) [hp : I.is_prime] :
Type u_1

Given a prime ideal P, localization.at_prime S P is a localization of R at the complement of P, as a quotient type.

theorem is_localization.at_prime.nontrivial {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hp : I.is_prime] [is_localization.at_prime S I] :
theorem is_localization.at_prime.local_ring {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hp : I.is_prime] [is_localization.at_prime S I] :
@[protected, instance]

The localization of R at the complement of a prime ideal is a local ring.

@[protected, instance]

The localization of an integral domain at the complement of a prime ideal is an integral domain.

theorem is_localization.at_prime.is_unit_to_map_iff {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) :
theorem is_localization.at_prime.to_map_mem_maximal_iff {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) (h : local_ring S := _) :
theorem is_localization.at_prime.is_unit_mk'_iff {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) (y : (I.prime_compl)) :
theorem is_localization.at_prime.mk'_mem_maximal_iff {R : Type u_1} [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (I : ideal R) [hI : I.is_prime] [is_localization.at_prime S I] (x : R) (y : (I.prime_compl)) (h : local_ring S := _) :

The unique maximal ideal of the localization at I.prime_compl lies over the ideal I.

The image of I in the localization at I.prime_compl is a maximal ideal, and in particular it is the unique maximal ideal given by the local ring structure at_prime.local_ring

theorem localization.le_comap_prime_compl_iff {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] {I : ideal R} [hI : I.is_prime] {J : ideal P} [hJ : J.is_prime] {f : R →+* P} :
noncomputable def localization.local_ring_hom {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) :

For a ring hom f : R →+* S and a prime ideal J in S, the induced ring hom from the localization of R at J.comap f to the localization of S at J.

To make this definition more flexible, we allow any ideal I of R as input, together with a proof that I = J.comap f. This can be useful when I is not definitionally equal to J.comap f.

Equations
Instances for localization.local_ring_hom
theorem localization.local_ring_hom_to_map {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) (x : R) :
theorem localization.local_ring_hom_mk' {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) (x : R) (y : (I.prime_compl)) :
@[protected, instance]
def localization.is_local_ring_hom_local_ring_hom {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) :
theorem localization.local_ring_hom_unique {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (I : ideal R) [hI : I.is_prime] (J : ideal P) [hJ : J.is_prime] (f : R →+* P) (hIJ : I = ideal.comap f J) {j : localization.at_prime I →+* localization.at_prime J} (hj : ∀ (x : R), j ((algebra_map R (localization.at_prime I)) x) = (algebra_map P (localization.at_prime J)) (f x)) :
@[simp]
theorem localization.local_ring_hom_comp {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (I : ideal R) [hI : I.is_prime] {S : Type u_2} [comm_semiring S] (J : ideal S) [hJ : J.is_prime] (K : ideal P) [hK : K.is_prime] (f : R →+* S) (hIJ : I = ideal.comap f J) (g : S →+* P) (hJK : J = ideal.comap g K) :