# 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.

Equations
• = ∀ {R : Type u} [hR : ] (M : ) (S : Type u) [hS : ] [inst : Algebra R S] [inst : ], P RP S
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.

Equations
• = ∀ (R : Type u) [inst : ], (∀ (J : ) (x : J.IsMaximal), P )P R
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• = ∀ ⦃R S : Type u⦄ [inst : ] [inst_1 : ] (f : R →+* S) (s : Set R), (∀ (r : s), P ())P f
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ᵣ.

Equations
• = ∀ ⦃R : Type u⦄ (S : Type u) [inst : ] [inst_1 : ] [inst_2 : Algebra R S] (r : R) [inst_3 : ], P ()
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
structure RingHom.PropertyIsLocal (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) :

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ᵣ).

• LocalizationPreserves :
• OfLocalizationSpanTarget :
• StableUnderComposition :
• HoldsForLocalizationAway :
Instances For
theorem RingHom.PropertyIsLocal.LocalizationPreserves {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (self : ) :
theorem RingHom.PropertyIsLocal.OfLocalizationSpanTarget {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (self : ) :
theorem RingHom.PropertyIsLocal.StableUnderComposition {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (self : ) :
theorem RingHom.PropertyIsLocal.HoldsForLocalizationAway {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (self : ) :
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 f) :
theorem RingHom.PropertyIsLocal.ofLocalizationSpan {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : ) :
theorem RingHom.OfLocalizationSpanTarget.ofIsLocalization {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : RingHom.OfLocalizationSpanTarget fun {R S : Type u} [] [] => P) (hP' : RingHom.RespectsIso fun {R S : Type u} [] [] => P) {R : Type u} {S : Type u} [] [] (f : R →+* S) (s : Set S) (hs : ) (hT : ∀ (r : s), ∃ (T : Type u) (x : ) (x_1 : Algebra S T) (_ : IsLocalization.Away (r) T), P (().comp f)) :
P f
theorem Ideal.le_of_localization_maximal {R : Type u} [] {I : } {J : } (h : ∀ (P : ) (hP : P.IsMaximal), 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 : P.IsMaximal), 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 : J.IsMaximal), 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 : J.IsMaximal), ) :
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 : J.IsMaximal), () r = 0) :
r = 0
theorem localization_isReduced :
LocalizationPreserves fun (R : Type u_1) (hR : ) =>
instance instIsReducedLocalization {R : Type u} [] (M : ) [] :
Equations
• =
theorem localizationPreserves_surjective :
RingHom.LocalizationPreserves fun {R S : Type u_1} (x : ) (x_1 : ) (f : R →+* S) =>
theorem surjective_ofLocalizationSpan :
RingHom.OfLocalizationSpan fun {R S : Type u_1} (x : ) (x_1 : ) (f : R →+* S) =>
theorem Module.Finite_of_isLocalization (R : Type u_1) (S : Type u_2) (Rₚ : Type u_3) (Sₚ : Type u_4) [] [] [CommRing Rₚ] [CommRing Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : ) [] [] [hRS : ] :
Module.Finite Rₚ Sₚ

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 : f.Finite) :
(IsLocalization.Away.map R' S' f r).Finite
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), 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 : M), 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 : M), 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 : f.FiniteType) :
(IsLocalization.Away.map R' S' f r).FiniteType
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), 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), 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.