Local properties of commutative rings

In this file, we define local properties in general.

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 definitions

• LocalizationPreserves : A property P of comm rings is said to be preserved by localization if P holds for M⁻¹R whenever P holds for R.
• OfLocalizationMaximal : A property P of comm rings satisfies OfLocalizationMaximal if P holds for R whenever P holds for Rₘ for all maximal ideal m.
• RingHom.LocalizationPreserves : 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.
• RingHom.OfLocalizationSpan : A property P of ring homs satisfies RingHom.OfLocalizationSpan if P holds for R →+* S whenever there exists a set { r } that spans R such that P holds for Rᵣ →+* Sᵣ.

Main results

• The triviality of an ideal or an element: ideal_eq_bot_of_localization, eq_zero_of_localization

def LocalizationPreserves (P : (R : Type u) → [inst : CommRing R] → Prop) : 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

• LocalizationPreserves P = ∀ {R : Type ?u.21} [hR : CommRing R] (M : Submonoid R) (S : Type ?u.21) [hS : CommRing S] [inst : Algebra R S] [inst : IsLocalization M S], P R → P S

def OfLocalizationMaximal (P : (R : Type u) → [inst : CommRing R] → Prop) : 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

• OfLocalizationMaximal P = ∀ (R : Type ?u.18) [inst : CommRing R], (∀ (J : Ideal R) (x : J.IsMaximal), P (Localization.AtPrime J)) → P R

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

A property P of ring homs is said to contain identities if P holds for the identity homomorphism of every ring.

Equations

• RingHom.ContainsIdentities P = ∀ (R : Type ?u.21) [inst : CommRing R], P (RingHom.id R)

def RingHom.LocalizationPreserves (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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.

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

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

Equations

• One or more equations did not get rendered due to their size.

def RingHom.OfLocalizationFiniteSpan (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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.

def RingHom.OfLocalizationSpan (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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

• RingHom.OfLocalizationSpan P = ∀ ⦃R S : Type ?u.30⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap f ↑r)) → P f

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

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

Equations

• One or more equations did not get rendered due to their size.

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

A property P of ring homs satisfies RingHom.StableUnderCompositionWithLocalizationAwaySource if whenever P holds for f it also holds for the composition with localization maps on the source.

Equations

• One or more equations did not get rendered due to their size.

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

A property P of ring homs satisfies RingHom.StableUnderCompositionWithLocalizationAway if whenever P holds for f it also holds for the composition with localization maps on the target.

Equations

• One or more equations did not get rendered due to their size.

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

A property P of ring homs satisfies RingHom.StableUnderCompositionWithLocalizationAway if whenever P holds for f it also holds for the composition with localization maps on the left and on the right.

Equations

• One or more equations did not get rendered due to their size.

def RingHom.OfLocalizationFiniteSpanTarget (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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.

def RingHom.OfLocalizationSpanTarget (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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.

def RingHom.OfLocalizationPrime (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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.

structure RingHom.PropertyIsLocal (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : 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ᵣ).

• localizationAwayPreserves : RingHom.LocalizationAwayPreserves P
• ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget P
• ofLocalizationSpan : RingHom.OfLocalizationSpan P
• StableUnderCompositionWithLocalizationAwayTarget : RingHom.StableUnderCompositionWithLocalizationAwayTarget P

theorem RingHom.ofLocalizationSpan_iff_finite (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : RingHom.OfLocalizationSpan P ↔ RingHom.OfLocalizationFiniteSpan P

theorem RingHom.ofLocalizationSpanTarget_iff_finite (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : RingHom.OfLocalizationSpanTarget P ↔ RingHom.OfLocalizationFiniteSpanTarget P

theorem RingHom.HoldsForLocalizationAway.of_bijective {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (H : RingHom.HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) (hf : Function.Bijective ⇑f) : P f

theorem RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPc : RingHom.StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPl : RingHom.HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem RingHom.HoldsForLocalizationAway.containsIdentities {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPl : RingHom.HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem RingHom.LocalizationAwayPreserves.respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem RingHom.StableUnderCompositionWithLocalizationAway.respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem RingHom.PropertyIsLocal.respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) : RingHom.RespectsIso P

theorem RingHom.LocalizationPreserves.away {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (H : RingHom.LocalizationPreserves P) : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem RingHom.PropertyIsLocal.HoldsForLocalizationAway {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) (hPi : RingHom.ContainsIdentities fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.HoldsForLocalizationAway P

theorem RingHom.OfLocalizationSpanTarget.ofLocalizationSpan {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.OfLocalizationSpanTarget P) (hP' : RingHom.StableUnderCompositionWithLocalizationAwaySource P) : RingHom.OfLocalizationSpan P

theorem RingHom.OfLocalizationSpan.ofIsLocalization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.OfLocalizationSpan fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤) (hT : ∀ (r : ↑s), ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ) (fᵣ : Rᵣ →+* Sᵣ) (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ) : P f

theorem RingHom.OfLocalizationSpan.ofIsLocalization' {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.OfLocalizationSpan fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤) (hT : ∀ (r : ↑s), ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra R Rᵣ) (x_3 : Algebra S Sᵣ) (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ), P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)) : P f

Variant of RingHom.OfLocalizationSpan.ofIsLocalization where fᵣ = IsLocalization.Away.map.

theorem RingHom.OfLocalizationSpanTarget.ofIsLocalization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.OfLocalizationSpanTarget fun {R S : Type u} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ⊤) (hT : ∀ (r : ↑s), ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)) : P f

theorem RingHom.IsStableUnderBaseChange.of_isLocalization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ] [Algebra S Sᵣ] [Algebra R S] [Algebra R Sᵣ] [Algebra Rᵣ Sᵣ] [IsScalarTower R S Sᵣ] [IsScalarTower R Rᵣ Sᵣ] (M : Submonoid R) [IsLocalization M Rᵣ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ] (h : P (algebraMap R S)) : P (algebraMap Rᵣ Sᵣ)

Let S be an R-algebra and Sᵣ and Rᵣ be the respective localizations at a submonoid M of R. If P is stable under base change and P holds for algebraMap R S, then P holds for algebraMap Rᵣ Sᵣ.

theorem RingHom.IsStableUnderBaseChange.isLocalization_map {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ] [Algebra S Sᵣ] (M : Submonoid R) [IsLocalization M Rᵣ] (f : R →+* S) [IsLocalization (Submonoid.map f M) Sᵣ] (hf : P f) : P (IsLocalization.map Sᵣ f ⋯)

If P is stable under base change and holds for f, then P holds for f localized at any submonoid M of R.

theorem RingHom.IsStableUnderBaseChange.localizationPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) : RingHom.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem Ideal.localized'_eq_map {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (I : Ideal R) : Submodule.localized' S p (Algebra.linearMap R S) I = Ideal.map (algebraMap R S) I

theorem Ideal.localized₀_eq_restrictScalars_map {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (I : Ideal R) : Submodule.localized₀ p (Algebra.linearMap R S) I = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)

theorem Algebra.idealMap_eq_ofEq_comp_toLocalized₀ {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (I : Ideal R) : Algebra.idealMap S I = ↑(LinearEquiv.ofEq (Submodule.localized₀ p (Algebra.linearMap R S) I) (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯) ∘ₗ Submodule.toLocalized₀ p (Algebra.linearMap R S) I

theorem Ideal.mem_of_localization_maximal {R : Type u_1} [CommSemiring R] {r : R} {J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), (algebraMap R (Localization.AtPrime P)) r ∈ Ideal.map (algebraMap R (Localization.AtPrime P)) J) : r ∈ J

theorem Ideal.le_of_localization_maximal {R : Type u_1} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ Ideal.map (algebraMap R (Localization.AtPrime P)) 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_1} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) 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_1} [CommSemiring R] (I : Ideal R) (h : ∀ (J : Ideal R) (x : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) : I = ⊥

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

theorem eq_zero_of_localization {R : Type u_1} [CommSemiring R] (r : R) (h : ∀ (J : Ideal R) (x : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0) : r = 0

theorem ideal_eq_bot_of_localization {R : Type u_1} [CommSemiring R] (I : Ideal R) (h : ∀ (J : Ideal R) (x : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥) : I = ⊥

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