# Documentation

Mathlib.RingTheory.LocalProperties

# Local properties of commutative rings #

In this file, we provide the proofs of various local properties.

## Naming Conventions #

• localization_P : P holds for S⁻¹R if P holds for R.
• P_of_localization_maximal : P holds for R if P holds for Rₘ for all maximal m.
• P_of_localization_prime : P holds for R if P holds for Rₘ for all prime m.
• P_ofLocalizationSpan : P holds for R if given a spanning set {fᵢ}, P holds for all R_{fᵢ}.

## Main results #

The following properties are covered:

• The triviality of an ideal or an element: ideal_eq_bot_of_localization, eq_zero_of_localization
• isReduced : localization_isReduced, isReduced_of_localization_maximal.
• finite: localization_finite, finite_ofLocalizationSpan
• finiteType: localization_finiteType, finiteType_ofLocalizationSpan
def LocalizationPreserves (P : (R : Type u) → [inst : ] → Prop) :

A property P of comm rings is said to be preserved by localization if P holds for M⁻¹R whenever P holds for R.

Instances For
def OfLocalizationMaximal (P : (R : Type u) → [inst : ] → Prop) :

A property P of comm rings satisfies OfLocalizationMaximal if P holds for R whenever P holds for Rₘ for all maximal ideal m.

Instances For
def RingHom.LocalizationPreserves (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs is said to be preserved by localization if P holds for M⁻¹R →+* M⁻¹S whenever P holds for R →+* S.

Instances For
def RingHom.OfLocalizationFiniteSpan (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs satisfies RingHom.OfLocalizationFiniteSpan if P holds for R →+* S whenever there exists a finite set { r } that spans R such that P holds for Rᵣ →+* Sᵣ.

Note that this is equivalent to RingHom.OfLocalizationSpan via RingHom.ofLocalizationSpan_iff_finite, but this is easier to prove.

Instances For
def RingHom.OfLocalizationSpan (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs satisfies RingHom.OfLocalizationFiniteSpan if P holds for R →+* S whenever there exists a set { r } that spans R such that P holds for Rᵣ →+* Sᵣ.

Note that this is equivalent to RingHom.OfLocalizationFiniteSpan via RingHom.ofLocalizationSpan_iff_finite, but this has less restrictions when applying.

Instances For
def RingHom.HoldsForLocalizationAway (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs satisfies RingHom.HoldsForLocalizationAway if P holds for each localization map R →+* Rᵣ.

Instances For
def RingHom.OfLocalizationFiniteSpanTarget (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs satisfies RingHom.OfLocalizationFiniteSpanTarget if P holds for R →+* S whenever there exists a finite set { r } that spans S such that P holds for R →+* Sᵣ.

Note that this is equivalent to RingHom.OfLocalizationSpanTarget via RingHom.ofLocalizationSpanTarget_iff_finite, but this is easier to prove.

Instances For
def RingHom.OfLocalizationSpanTarget (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs satisfies RingHom.OfLocalizationSpanTarget if P holds for R →+* S whenever there exists a set { r } that spans S such that P holds for R →+* Sᵣ.

Note that this is equivalent to RingHom.OfLocalizationFiniteSpanTarget via RingHom.ofLocalizationSpanTarget_iff_finite, but this has less restrictions when applying.

Instances For
def RingHom.OfLocalizationPrime (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

A property P of ring homs satisfies RingHom.OfLocalizationPrime if P holds for R whenever P holds for Rₘ for all prime ideals p.

Instances For
structure RingHom.PropertyIsLocal (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :
• LocalizationPreserves :
• OfLocalizationSpanTarget :
• StableUnderComposition :
• HoldsForLocalizationAway :

A property of ring homs is local if it is preserved by localizations and compositions, and for each { r } that spans S, we have P (R →+* S) ↔ ∀ r, P (R →+* Sᵣ).

Instances For
theorem RingHom.ofLocalizationSpan_iff_finite (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :
theorem RingHom.ofLocalizationSpanTarget_iff_finite (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :
theorem RingHom.PropertyIsLocal.respectsIso {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) :
theorem RingHom.LocalizationPreserves.away {R : Type u} {S : Type u} [] [] {R' : Type u} {S' : Type u} [CommRing R'] [CommRing S'] {f : R →+* S} [Algebra R R'] [Algebra S S'] {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (r : R) [] [IsLocalization.Away (f r) S'] (hf : P R S inst✝ inst✝¹ f) :
P R' S' inst✝ inst✝¹ (IsLocalization.Away.map R' S' f r)
theorem RingHom.PropertyIsLocal.ofLocalizationSpan {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) :
theorem Ideal.le_of_localization_maximal {R : Type u} [] {I : } {J : } (h : ∀ (P : ) (hP : ), Ideal.map () I Ideal.map () J) :
I J

Let I J : Ideal R. If the localization of I at each maximal ideal P is included in the localization of J at P, then I ≤ J.

theorem Ideal.eq_of_localization_maximal {R : Type u} [] {I : } {J : } (h : ∀ (P : ) (x : ), Ideal.map () I = Ideal.map () J) :
I = J

Let I J : Ideal R. If the localization of I at each maximal ideal P is equal to the localization of J at P, then I = J.

theorem ideal_eq_bot_of_localization' {R : Type u} [] (I : ) (h : ∀ (J : ) (hJ : ), Ideal.map () I = ) :
I =

An ideal is trivial if its localization at every maximal ideal is trivial.

theorem ideal_eq_bot_of_localization {R : Type u} [] (I : ) (h : ∀ (J : ) (hJ : ), ) :
I =

An ideal is trivial if its localization at every maximal ideal is trivial.

theorem eq_zero_of_localization {R : Type u} [] (r : R) (h : ∀ (J : ) (hJ : ), ↑() r = 0) :
r = 0

If S is a finite R-algebra, then S' = M⁻¹S is a finite R' = M⁻¹R-algebra.

theorem localization_away_map_finite {R : Type u} {S : Type u} [] [] (R' : Type u) (S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) [Algebra R R'] [Algebra S S'] (r : R) [] [IsLocalization.Away (f r) S'] (hf : ) :
theorem IsLocalization.smul_mem_finsetIntegerMultiple_span {R : Type u} {S : Type u} [] [] (M : ) (S' : Type u) [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map () M) S'] (x : S) (s : Finset S') (hx : ↑(algebraMap S S') x ) :
m, m x

Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S. If the image of some x : S falls in the span of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the span of IsLocalization.finsetIntegerMultiple _ s over R.

theorem multiple_mem_span_of_mem_localization_span {R : Type u} {S : Type u} [] [] (M : ) (R' : Type u) [CommRing R'] [Algebra R R'] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S] [] (s : Set S) (x : S) (hx : x ) :
t, t x

If S is an R' = M⁻¹R algebra, and x ∈ span R' s, then t • x ∈ span R s for some t : M.

theorem multiple_mem_adjoin_of_mem_localization_adjoin {R : Type u} {S : Type u} [] [] (M : ) (R' : Type u) [CommRing R'] [Algebra R R'] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S] [] (s : Set S) (x : S) (hx : x ) :
t, t x

If S is an R' = M⁻¹R algebra, and x ∈ adjoin R' s, then t • x ∈ adjoin R s for some t : M.

theorem localization_away_map_finiteType {R : Type u} {S : Type u} [] [] (R' : Type u) (S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) [Algebra R R'] [Algebra S S'] (r : R) [] [IsLocalization.Away (f r) S'] (hf : ) :
theorem IsLocalization.exists_smul_mem_of_mem_adjoin {R : Type u} {S : Type u} [] [] {S' : Type u} [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] (M : ) [] (x : S) (s : Finset S') (A : ) (hA₁ : ) (hA₂ : M A.toSubmonoid) (hx : ↑(algebraMap S S') x ) :
m, m x A

Let S be an R-algebra, M a submonoid of S, S' = M⁻¹S. Suppose the image of some x : S falls in the adjoin of some finite s ⊆ S' over R, and A is an R-subalgebra of S containing both M and the numerators of s. Then, there exists some m : M such that m • x falls in A.

theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple {R : Type u} {S : Type u} [] [] (M : ) {S' : Type u} [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map () M) S'] (x : S) (s : Finset S') (hx : ↑(algebraMap S S') x ) :
m, m x

Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S. If the image of some x : S falls in the adjoin of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the adjoin of IsLocalization.finsetIntegerMultiple _ s over R.