Documentation

Mathlib.RingTheory.LocalProperties.Basic

Local properties of commutative rings #

In this file, we define local properties in general.

Naming Conventions #

Main definitions #

Main results #

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

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

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

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

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

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

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

theorem RingHom.PropertyIsLocal.LocalizationPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (self : RingHom.PropertyIsLocal P) :
theorem RingHom.HoldsForLocalizationAway.of_bijective {R : Type u} {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.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) :
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) :
theorem RingHom.LocalizationPreserves.away {R : Type u} {S : Type u} [CommRing R] [CommRing S] {f : R →+* S} {R' : Type u} {S' : Type u} [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (H : RingHom.LocalizationPreserves P) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : P f) :
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) :
theorem RingHom.PropertyIsLocal.ofLocalizationSpan {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.PropertyIsLocal P) :
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 : Type u} {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.StableUnderBaseChange.of_isLocalization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.StableUnderBaseChange P) {R : Type u} {S : Type u} {Rᵣ : Type u} {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.StableUnderBaseChange.isLocalization_map {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.StableUnderBaseChange P) {R : Type u} {S : Type u} {Rᵣ : Type u} {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.StableUnderBaseChange.localizationPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.StableUnderBaseChange P) :
theorem Ideal.le_of_localization_maximal {R : Type u} [CommRing R] {I : Ideal R} {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} [CommRing R] {I : Ideal R} {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} [CommRing 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 ideal_eq_bot_of_localization {R : Type u} [CommRing 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.

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