Documentation

Mathlib.RingTheory.Localization.AtPrime

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

Main definitions #

Main results #

Implementation notes #

See RingTheory.Localization.Basic for a design overview.

Tags #

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

@[reducible, inline]
abbrev IsLocalization.AtPrime {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] :

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

Equations
@[reducible, inline]
abbrev Localization.AtPrime {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] :
Type u_1

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

Equations
@[deprecated IsLocalization.AtPrime.isLocalRing (since := "2024-11-09")]

Alias of IsLocalization.AtPrime.isLocalRing.

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

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

The prime ideals in the localization of a commutative ring at a prime ideal I are in order-preserving bijection with the prime ideals contained in I.

Equations
  • One or more equations did not get rendered due to their size.
theorem IsLocalization.AtPrime.isUnit_to_map_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) :
theorem IsLocalization.AtPrime.isUnit_mk'_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : I.primeCompl) :
theorem IsLocalization.AtPrime.mk'_mem_maximal_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : I.primeCompl) (h : IsLocalRing S := ) :

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

The image of I in the localization at I.primeCompl is a maximal ideal, and in particular it is the unique maximal ideal given by the local ring structure AtPrime.isLocalRing

noncomputable def Localization.localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (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
theorem Localization.localRingHom_to_map {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) :
theorem Localization.localRingHom_mk' {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) (y : I.primeCompl) :
instance Localization.isLocalHom_localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) :
@[deprecated Localization.isLocalHom_localRingHom (since := "2024-10-10")]
theorem Localization.isLocalRingHom_localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) :

Alias of Localization.isLocalHom_localRingHom.

theorem Localization.localRingHom_unique {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) {j : Localization.AtPrime I →+* Localization.AtPrime J} (hj : ∀ (x : R), j ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)) :
localRingHom I J f hIJ = j
theorem Localization.localRingHom_comp {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] {S : Type u_4} [CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P) [hK : K.IsPrime] (f : R →+* S) (hIJ : I = Ideal.comap f J) (g : S →+* P) (hJK : J = Ideal.comap g K) :
localRingHom I K (g.comp f) = (localRingHom J K g hJK).comp (localRingHom I J f hIJ)
@[reducible, inline]
noncomputable abbrev Localization.AtPrime.mapPiEvalRingHom {ι : Type u_4} {R : ιType u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] :

Localization.localRingHom specialized to a projection homomorphism from a product ring.

Equations
theorem Localization.AtPrime.mapPiEvalRingHom_bijective {ι : Type u_4} {R : ιType u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] :
theorem Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap {ι : Type u_4} {R : ιType u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] :
theorem Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply {ι : Type u_4} {R : ιType u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] {r : (i : ι) → R i} :
theorem Ideal.isPrime_map_of_isLocalizationAtPrime {R : Type u_4} [CommRing R] (q : Ideal R) [q.IsPrime] {S : Type u_5} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime] (hpq : p q) :
theorem Ideal.under_map_of_isLocalizationAtPrime {R : Type u_4} [CommRing R] (q : Ideal R) [q.IsPrime] {S : Type u_5} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime] (hpq : p q) :
under R (map (algebraMap R S) p) = p