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 : 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} [hR : CommRing R] (M : Submonoid R) (S : Type u) [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) [inst : CommRing R], (∀ (J : Ideal R) (x : J.IsMaximal), P (Localization.AtPrime J)) → P 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.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⦄ [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

• RingHom.HoldsForLocalizationAway P = ∀ ⦃R : Type u⦄ (S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R) [inst_3 : IsLocalization.Away r S], P (algebraMap R S)

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

• LocalizationPreserves : RingHom.LocalizationPreserves P
• OfLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget P
• StableUnderComposition : RingHom.StableUnderComposition P
• HoldsForLocalizationAway : RingHom.HoldsForLocalizationAway P

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

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

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

theorem RingHom.PropertyIsLocal.HoldsForLocalizationAway {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (self : RingHom.PropertyIsLocal P) : RingHom.HoldsForLocalizationAway 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 : 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.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 {R : Type u} {S : Type u} [CommRing R] [CommRing S] {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 : 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) : P (IsLocalization.Away.map R' S' f r)

theorem RingHom.PropertyIsLocal.ofLocalizationSpan {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.PropertyIsLocal P) : RingHom.OfLocalizationSpan 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 Ideal.le_of_localization_maximal {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : ∀ (P : Ideal R) (hP : 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) (hJ : 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) (hJ : 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) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0) : r = 0

theorem localization_isReduced : LocalizationPreserves fun (R : Type u_1) (hR : CommRing R) => IsReduced R

instance instIsReducedLocalization {R : Type u} [CommRing R] (M : Submonoid R) [IsReduced R] : IsReduced (Localization M)

Equations

• ⋯ = ⋯

theorem isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun (R : Type u_1) (hR : CommRing R) => IsReduced R

theorem localizationPreserves_surjective : RingHom.LocalizationPreserves fun {R S : Type u_1} (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) => Function.Surjective ⇑f

theorem surjective_ofLocalizationSpan : RingHom.OfLocalizationSpan fun {R S : Type u_1} (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) => Function.Surjective ⇑f

theorem surjective_localRingHom_of_surjective {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Function.Surjective ⇑f) (P : Ideal S) [P.IsPrime] : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)

A surjective ring homomorphism R →+* S induces a surjective homomorphism R_{f⁻¹(P)} →+* S_P for every prime ideal P of S.

theorem surjective_respectsIso : RingHom.RespectsIso fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Surjective ⇑f

theorem Module.Finite_of_isLocalization (R : Type u_1) (S : Type u_2) (Rₚ : Type u_3) (Sₚ : Type u_4) [CommSemiring R] [CommRing S] [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 : Submonoid R) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] : Module.Finite Rₚ Sₚ

theorem localization_finite : RingHom.LocalizationPreserves @RingHom.Finite

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} [CommRing R] [CommRing S] (R' : Type u) (S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) [Algebra R R'] [Algebra S S'] (r : R) [IsLocalization.Away 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} [CommRing R] [CommRing S] (M : Submonoid R) (S' : Type u) [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S') (hx : (algebraMap S S') x ∈ Submodule.span R ↑s) : ∃ (m : ↥M), m • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

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} [CommRing R] (M : Submonoid R) (R' : Type u) [CommRing R'] [Algebra R R'] {N : Type u_1} [AddCommMonoid N] [Module R N] [Module R' N] [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) (hx : x ∈ Submodule.span R' s) : ∃ (t : ↥M), t • x ∈ Submodule.span R s

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

theorem multiple_mem_adjoin_of_mem_localization_adjoin {R : Type u} {S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (R' : Type u) [CommRing R'] [Algebra R R'] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S) (hx : x ∈ Algebra.adjoin R' s) : ∃ (t : ↥M), t • x ∈ Algebra.adjoin R s

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

theorem finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite

theorem localization_finiteType : RingHom.LocalizationPreserves @RingHom.FiniteType

theorem localization_away_map_finiteType {R : Type u} {S : Type u} [CommRing R] [CommRing S] (R' : Type u) (S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) [Algebra R R'] [Algebra S S'] (r : R) [IsLocalization.Away 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} [CommRing R] [CommRing S] {S' : Type u} [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S') (A : Subalgebra R S) (hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A) (hA₂ : M ≤ A.toSubmonoid) (hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s) : ∃ (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} [CommRing R] [CommRing S] (M : Submonoid R) {S' : Type u} [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S') (hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s) : ∃ (m : ↥M), m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

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.

theorem finiteType_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.FiniteType