Localizations of commutative rings at the complement of a prime ideal #
Main definitions #
IsLocalization.AtPrime (P : Ideal R) [IsPrime P] (S : Type*)expresses thatSis a localization at (the complement of) a prime idealP, as an abbreviation ofIsLocalization P.prime_compl S
Main results #
IsLocalization.AtPrime.isLocalRing: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring
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
Instances For
@[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
Instances For
theorem
IsLocalization.AtPrime.nontrivial
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
@[deprecated IsLocalization.AtPrime.nontrivial (since := "2025-07-31")]
theorem
IsLocalization.AtPrime.Nontrivial
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
Alias of IsLocalization.AtPrime.nontrivial.
theorem
IsLocalization.AtPrime.isLocalRing
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
instance
Localization.AtPrime.isLocalRing
{R : Type u_1}
[CommSemiring R]
(P : Ideal R)
[hp : P.IsPrime]
:
The localization of R at the complement of a prime ideal is a local ring.
instance
Localization.instNoZeroSMulDivisorsAtPrimeAlgebraMapSubmonoidPrimeComplOfNoZeroDivisorsOfIsDomain
{R : Type u_4}
{S : Type u_5}
[CommRing R]
[NoZeroDivisors R]
{P : Ideal R}
[CommRing S]
[Algebra R S]
[NoZeroSMulDivisors R S]
[IsDomain S]
[P.IsPrime]
:
theorem
IsLocalization.AtPrime.faithfulSMul
(S : Type u_2)
[CommSemiring S]
(R : Type u_4)
[CommRing R]
[NoZeroDivisors R]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
FaithfulSMul R S
instance
Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors
{R : Type u_4}
[CommRing R]
[NoZeroDivisors R]
(P : Ideal R)
[hp : P.IsPrime]
:
theorem
IsLocalization.isDomain_of_atPrime
{A : Type u_4}
[CommRing A]
[IsDomain A]
(S : Type u_5)
[CommSemiring S]
[Algebra A S]
(P : Ideal A)
[P.IsPrime]
[IsLocalization.AtPrime S P]
:
IsDomain S
This is an IsLocalization.AtPrime version for IsLocalization.isDomain_of_local_atPrime.
def
IsLocalization.AtPrime.orderIsoOfPrime
{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]
:
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.
Instances For
@[simp]
theorem
IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe
{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]
(a✝ : { p : Ideal R // p.IsPrime ∧ p ≤ I })
:
↑↑((RelIso.symm (orderIsoOfPrime S I)) a✝) = ⋂ (s : Submodule S S),
⋂ (_ :
↑↑((OrderIso.setCongr (fun (p : Ideal R) => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p)
(fun (p : Ideal R) => p.IsPrime ∧ p ≤ I) ⋯).symm
a✝) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s),
↑s
@[simp]
theorem
IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe
{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]
(a✝ : { p : Ideal S // p.IsPrime })
:
def
IsLocalization.AtPrime.primeSpectrumOrderIso
{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]
:
The prime spectrum of the localization of a commutative ring R at a prime ideal I are in order-preserving bijection with the interval (-∞, I] in the prime spectrum of R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal
{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]
(a✝ : PrimeSpectrum S)
:
@[simp]
theorem
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal
{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]
(a✝ : ↑(Set.Iic { asIdeal := I, isPrime := hI }))
:
↑((RelIso.symm (primeSpectrumOrderIso S I)) a✝).asIdeal = ⋂ (s : Submodule S S),
⋂ (_ :
↑↑((OrderIso.setCongr (fun (p : Ideal R) => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p)
(fun (p : Ideal R) => p.IsPrime ∧ p ≤ I) ⋯).symm
⟨(↑a✝).asIdeal, ⋯⟩) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s),
↑s
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.to_map_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)
(h : IsLocalRing S := ⋯)
:
theorem
IsLocalization.AtPrime.comap_maximalIdeal
{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]
(h : IsLocalRing S := ⋯)
:
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 := ⋯)
:
theorem
Localization.AtPrime.comap_maximalIdeal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
:
Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I
The unique maximal ideal of the localization at I.primeCompl lies over the ideal I.
theorem
Localization.AtPrime.map_eq_maximalIdeal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
:
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
theorem
Localization.AtPrime.eq_maximalIdeal_iff_comap_eq
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
{J : Ideal (Localization.AtPrime I)}
:
Ideal.comap (algebraMap R (Localization.AtPrime I)) J = I ↔ J = IsLocalRing.maximalIdeal (Localization.AtPrime I)
theorem
Localization.le_comap_primeCompl_iff
{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}
:
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
- Localization.localRingHom I J f hIJ = IsLocalization.map (Localization.AtPrime J) f ⋯
Instances For
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)
:
(localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)
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)
:
(localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩
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)
:
IsLocalHom (localRingHom I J f hIJ)
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))
:
@[simp]
theorem
Localization.localRingHom_id
{R : Type u_1}
[CommSemiring R]
(I : Ideal R)
[hI : I.IsPrime]
:
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)
:
noncomputable instance
Localization.AtPrime.instAlgebraOfLiesOver
{A : Type u_4}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra A B]
(p : Ideal A)
[p.IsPrime]
(P : Ideal B)
[P.IsPrime]
[P.LiesOver p]
:
Equations
- Localization.AtPrime.instAlgebraOfLiesOver p P = (Localization.localRingHom p P (algebraMap A B) ⋯).toAlgebra
@[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
- Localization.AtPrime.mapPiEvalRingHom I = Localization.localRingHom (Ideal.comap (Pi.evalRingHom R i) I) I (Pi.evalRingHom R i) ⋯
Instances For
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]
:
(mapPiEvalRingHom I).comp (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) = (algebraMap (R i) (Localization.AtPrime I)).comp (Pi.evalRingHom R i)
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}
:
(mapPiEvalRingHom I) ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) r) = (algebraMap (R i) (Localization.AtPrime I)) (r i)
theorem
Ideal.isPrime_map_of_isLocalizationAtPrime
{R : Type u_1}
[CommSemiring R]
(q : Ideal R)
[q.IsPrime]
{S : Type u_4}
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S q]
{p : Ideal R}
[p.IsPrime]
(hpq : p ≤ q)
:
(map (algebraMap R S) p).IsPrime
theorem
Ideal.under_map_of_isLocalizationAtPrime
{R : Type u_1}
[CommSemiring R]
(q : Ideal R)
[q.IsPrime]
{S : Type u_4}
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S q]
{p : Ideal R}
[p.IsPrime]
(hpq : p ≤ q)
:
theorem
IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes
{R : Type u_5}
[CommSemiring R]
(p : Ideal R)
(hp : p ∈ minimalPrimes R)
(S : Type u_6)
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S p]
: