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

Main definitions #

IsLocalization.AtPrime (P : Ideal R) [IsPrime P] (S : Type*) expresses that S is a localization at (the complement of) a prime ideal P, as an abbreviation of IsLocalization 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

source

🔹 coverage

@[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] :

Prop

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.

Instances For

source

🔸 coverage

@[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.

Instances For

source

📐 coverage

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

Nontrivial S

source

📐 coverage

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

IsLocalRing S

source

📐 coverage

instance IsLocalization.isDomain_of_local_atPrime {A : Type u_4} [CommRing A] [IsDomain A] {P : Ideal A} (x✝ : P.IsPrime) :

IsDomain (Localization.AtPrime P)

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

source

📐 coverage

instance Localization.AtPrime.isLocalRing {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] :

IsLocalRing (Localization P.primeCompl)

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

source

📐 coverage

instance Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain {R : Type u_4} {S : Type u_5} [CommRing R] [IsDomain R] {P : Ideal R} [CommRing S] [Algebra R S] [Module.IsTorsionFree R S] [IsDomain S] [P.IsPrime] :

Module.IsTorsionFree (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))

source

📐 coverage

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

source

📐 coverage

instance Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors {R : Type u_4} [CommRing R] [NoZeroDivisors R] (P : Ideal R) [hp : P.IsPrime] :

FaithfulSMul R (Localization.AtPrime P)

source

📐 coverage

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.

source

🔸 coverage

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

{ p : Ideal S // p.IsPrime } ≃o { p : Ideal R // p.IsPrime ∧ p ≤ 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.

Instances For

source

📐 coverage

@[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

source

📐 coverage

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

↑↑((orderIsoOfPrime S I) a✝) = ⇑(algebraMap R S) ⁻¹' ↑↑a✝

source

🔸 coverage

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

PrimeSpectrum S ≃o ↑(Set.Iic { asIdeal := I, isPrime := hI })

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.

Instances For

source

📐 coverage

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

↑(↑((primeSpectrumOrderIso S I) a✝)).asIdeal = ⇑(algebraMap R S) ⁻¹' ↑a✝.asIdeal

source

📐 coverage

@[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

source

📐 coverage

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

IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl

source

📐 coverage

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

(algebraMap R S) x ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I

source

📐 coverage

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

Ideal.comap (algebraMap R S) (IsLocalRing.maximalIdeal S) = I

source

📐 coverage

instance IsLocalization.AtPrime.liesOver_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 := ⋯) :

(IsLocalRing.maximalIdeal S).LiesOver I

source

📐 coverage

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

IsUnit (mk' S x y) ↔ x ∈ I.primeCompl

source

📐 coverage

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

mk' S x y ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I

source

📐 coverage

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.

source

📐 coverage

theorem Localization.AtPrime.map_eq_maximalIdeal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] :

Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)

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

source

📐 coverage

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)

source

📐 coverage

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

I.primeCompl ≤ Submonoid.comap f J.primeCompl ↔ Ideal.comap f J ≤ I

source

🔸 coverage

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

Localization.AtPrime I →+* Localization.AtPrime 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.

Instances For

source

📐 coverage

@[simp]

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)

source

📐 coverage

@[simp]

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, ⋯⟩

source

📐 coverage

@[simp]

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) (mk x y) = mk (f x) ⟨f ↑y, ⋯⟩

source

📐 coverage

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)

source

📐 coverage

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

source

📐 coverage

@[simp]

theorem Localization.localRingHom_id {R : Type u_1} [CommSemiring R] (I : Ideal R) [hI : I.IsPrime] :

localRingHom I I (RingHom.id R) ⋯ = RingHom.id (Localization.AtPrime I)

source

📐 coverage

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)

source

🔸 coverage

noncomputable def Localization.localAlgHom {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [Algebra R P] (I : Ideal S) [I.IsPrime] (J : Ideal P) [J.IsPrime] (f : S →ₐ[R] P) (hIJ : I = Ideal.comap f J) :

Localization.AtPrime I →ₐ[R] Localization.AtPrime J

For an algebra hom f : S →ₐ[R] P and a prime ideal J in P, the induced ring hom from the localization of R at J ∩ S to the localization of P at J.

Instances For

source

📐 coverage

@[simp]

theorem Localization.localAlgHom_apply {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [Algebra R P] (I : Ideal S) [I.IsPrime] (J : Ideal P) [J.IsPrime] (f : S →ₐ[R] P) (hIJ : I = Ideal.comap f J) (x : Localization.AtPrime I) :

(localAlgHom I J f hIJ) x = (localRingHom I J f.toRingHom hIJ) x

source

📐 coverage

theorem Localization.localRingHom_bijective_of_saturated_inf_eq_top {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Ideal S} [P.IsPrime] {s : Subalgebra R S} (H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤) (p : Ideal ↥s) [p.IsPrime] [P.LiesOver p] :

Function.Bijective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

source

🔸 coverage

@[implicit_reducible]

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

Algebra (Localization.AtPrime p) (Localization.AtPrime P)

source

📐 coverage

instance Localization.AtPrime.instIsScalarTower {R : Type u_1} [CommSemiring R] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Algebra R A] [Algebra R B] [IsScalarTower R A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] :

IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime P)

source

📐 coverage

instance Localization.AtPrime.instIsScalarTower_1 {A : Type u_4} {B : Type u_5} {C : Type u_6} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] (Q : Ideal C) [Q.IsPrime] [Q.LiesOver P] [Q.LiesOver p] :

IsScalarTower (Localization.AtPrime p) (Localization.AtPrime P) (Localization.AtPrime Q)

source

🔸 coverage

@[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.AtPrime (Ideal.comap (Pi.evalRingHom R i) I) →+* Localization.AtPrime I

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

Instances For

source

📐 coverage

theorem Localization.AtPrime.mapPiEvalRingHom_bijective {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] :

Function.Bijective ⇑(mapPiEvalRingHom I)

source

📐 coverage

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)

source

📐 coverage

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)

source

📐 coverage

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

source

📐 coverage

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

under R (map (algebraMap R S) p) = p

source

📐 coverage

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

Subsingleton (PrimeSpectrum S)

source

📐 coverage

theorem IsLocalization.liesOver_of_isPrime_of_disjoint {R : Type u_1} [CommSemiring R] {S : Type u_4} [CommSemiring S] [Algebra R S] {R' : Type u_5} {S' : Type u_6} (M : Submonoid R) (T : Submonoid S) [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S'] [IsLocalization M R'] [IsLocalization T S'] (p : Ideal R) {P : Ideal S} [P.IsPrime] [P.LiesOver p] (disj : Disjoint ↑T ↑P) :

(Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)

If R' (resp. S') is the localization of R (resp. S) and P lies over p then the image of P in S' lies over the image of p in R'.

source

📐 coverage

theorem Ideal.IsMaximal.of_isLocalization_of_disjoint {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_4} [CommSemiring S] [Algebra R S] [IsLocalization M S] {J : Ideal S} [(comap (algebraMap R S) J).IsMaximal] :

J.IsMaximal

source

📐 coverage

theorem IsLocalization.AtPrime.isPrime_map_of_liesOver {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Sₚ : Type u_5) [CommSemiring Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsPrime] [P.LiesOver p] :

(Ideal.map (algebraMap S Sₚ) P).IsPrime

source

📐 coverage

theorem IsLocalization.AtPrime.map_eq_maximalIdeal {R : Type u_1} [CommSemiring R] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_4) [CommSemiring Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :

Ideal.map (algebraMap R Rₚ) p = IsLocalRing.maximalIdeal Rₚ

source

📐 coverage

instance IsLocalization.AtPrime.isMaximal_map {R : Type u_1} [CommSemiring R] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_4) [CommSemiring Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :

(Ideal.map (algebraMap R Rₚ) p).IsMaximal

source

📐 coverage

theorem IsLocalization.AtPrime.comap_map_of_isMaximal {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Sₚ : Type u_5) [CommSemiring Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsMaximal] [P.LiesOver p] :

Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P) = P

source

🔸 coverage

noncomputable def IsLocalization.AtPrime.equivQuotMaximalIdeal {R : Type u_7} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_8) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :

R ⧸ p ≃+* Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ

The isomorphism R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ, where Rₚ satisfies IsLocalization.AtPrime Rₚ p. In particular, localization preserves the residue field.

Instances For

source

📐 coverage

@[simp]

theorem IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk {R : Type u_7} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_8) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (x : R) :

(equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ)) ((algebraMap R Rₚ) x)

source

📐 coverage

@[simp]

theorem IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk {R : Type u_7} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_8) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (x : R) (s : ↥p.primeCompl) :

(equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ)) (mk' Rₚ x s)) = (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s)⁻¹

source

🔸 coverage

@[deprecated IsLocalization.AtPrime.equivQuotMaximalIdeal (since := "2025-11-13")]

def equivQuotMaximalIdealOfIsLocalization {R : Type u_7} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_8) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :

R ⧸ p ≃+* Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ

Alias of IsLocalization.AtPrime.equivQuotMaximalIdeal.

The isomorphism R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ, where Rₚ satisfies IsLocalization.AtPrime Rₚ p. In particular, localization preserves the residue field.

Instances For

source

📐 coverage

theorem IsLocalization.AtPrime.comap_map_eq_map {S : Type u_6} {R : Type u_7} [CommRing R] (p : Ideal R) [p.IsMaximal] {Sₚ : Type u_9} [CommRing S] [Algebra R S] [CommRing Sₚ] [Algebra S Sₚ] [Algebra R Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [IsScalarTower R S Sₚ] :

Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap R Sₚ) p) = Ideal.map (algebraMap R S) p

source

🔸 coverage

noncomputable def IsLocalization.AtPrime.equivQuotientMapMaximalIdeal (S : Type u_6) {R : Type u_7} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_8) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Sₚ : Type u_9) [CommRing S] [Algebra R S] [CommRing Sₚ] [Algebra S Sₚ] [Algebra R Sₚ] [Algebra Rₚ Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [p.IsMaximal] :

S ⧸ Ideal.map (algebraMap R S) p ≃+* Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ)

The isomorphism S ⧸ pS ≃+* Sₚ ⧸ p·Sₚ, where Sₚ is the localization of S at the (image) of the complement of p

Instances For

source

📐 coverage

theorem IsLocalization.AtPrime.map_eq_top_of_not_le {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {I p : Ideal R} [p.IsPrime] [IsLocalization.AtPrime S p] (hle : ¬I ≤ p) :

Ideal.map (algebraMap R S) I = ⊤

Documentation

Mathlib.RingTheory.Localization.AtPrime.Basic

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

Main definitions #

Main results #

Implementation notes #

Tags #