mathlib3 documentation

ring_theory.local_properties

Local properties of commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Naming Conventions #

Main results #

The following properties are covered:

source
def localization_preserves (P : Π (R : Type u) [_inst_7 : comm_ring 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
source
def of_localization_maximal (P : Π (R : Type u) [_inst_7 : comm_ring R], Prop) :
Prop

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

Equations
source
def ring_hom.localization_preserves (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring 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
source
def ring_hom.of_localization_finite_span (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
Prop

A property P of ring homs satisfies ring_hom.of_localization_finite_span 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 ring_hom.of_localization_span via ring_hom.of_localization_span_iff_finite, but this is easier to prove.

Equations
source
def ring_hom.of_localization_span (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
Prop

A property P of ring homs satisfies ring_hom.of_localization_finite_span 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 ring_hom.of_localization_finite_span via ring_hom.of_localization_span_iff_finite, but this has less restrictions when applying.

Equations
source
def ring_hom.holds_for_localization_away (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
Prop

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

Equations
source
def ring_hom.of_localization_finite_span_target (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
Prop

A property P of ring homs satisfies ring_hom.of_localization_finite_span_target 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 ring_hom.of_localization_span_target via ring_hom.of_localization_span_target_iff_finite, but this is easier to prove.

Equations
source
def ring_hom.of_localization_span_target (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
Prop

A property P of ring homs satisfies ring_hom.of_localization_span_target 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 ring_hom.of_localization_finite_span_target via ring_hom.of_localization_span_target_iff_finite, but this has less restrictions when applying.

Equations
source
def ring_hom.of_localization_prime (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
Prop

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

Equations
source
structure ring_hom.property_is_local (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring 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ᵣ).

source
theorem ring_hom.of_localization_span_iff_finite (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
ring_hom.of_localization_span P ↔ ring_hom.of_localization_finite_span P
source
theorem ring_hom.of_localization_span_target_iff_finite (P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop) :
ring_hom.of_localization_span_target P ↔ ring_hom.of_localization_finite_span_target P
source
theorem ring_hom.property_is_local.respects_iso {P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) :
ring_hom.respects_iso P
source
theorem ring_hom.localization_preserves.away {R S : Type u} [comm_ring R] [comm_ring S] {R' S' : Type u} [comm_ring R'] [comm_ring S'] {f : R →+* S} [algebra R R'] [algebra S S'] {P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop} (H : ring_hom.localization_preserves P) (r : R) [is_localization.away r R'] [is_localization.away (⇑f r) S'] (hf : P f) :
P (is_localization.away.map R' S' f r)
source
theorem ring_hom.property_is_local.of_localization_span {P : Π {R S : Type u} [_inst_7 : comm_ring R] [_inst_8 : comm_ring S], (R →+* S) → Prop} (hP : ring_hom.property_is_local P) :
ring_hom.of_localization_span P
source
theorem ideal.le_of_localization_maximal {R : Type u} [comm_ring R] {I J : ideal R} (h : ∀ (P : ideal R) (hP : P.is_maximal), ideal.map (algebra_map R (localization.at_prime P)) I ≤ ideal.map (algebra_map R (localization.at_prime 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.

source
theorem ideal.eq_of_localization_maximal {R : Type u} [comm_ring R] {I J : ideal R} (h : ∀ (P : ideal R) (hP : P.is_maximal), ideal.map (algebra_map R (localization.at_prime P)) I = ideal.map (algebra_map R (localization.at_prime 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.

source
theorem ideal_eq_bot_of_localization' {R : Type u} [comm_ring R] (I : ideal R) (h : ∀ (J : ideal R) (hJ : J.is_maximal), ideal.map (algebra_map R (localization.at_prime J)) I = ⊥) :
I = ⊥

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

source
theorem ideal_eq_bot_of_localization {R : Type u} [comm_ring R] (I : ideal R) (h : ∀ (J : ideal R) (hJ : J.is_maximal), is_localization.coe_submodule (localization.at_prime J) I = ⊥) :
I = ⊥

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

source
theorem eq_zero_of_localization {R : Type u} [comm_ring R] (r : R) (h : ∀ (J : ideal R) (hJ : J.is_maximal), ⇑(algebra_map R (localization.at_prime J)) r = 0) :
r = 0
source
theorem localization_is_reduced  :
localization_preserves (λ (R : Type u_1) (hR : comm_ring R), is_reduced R)
source
@[protected, instance]
def localization.is_reduced {R : Type u} [comm_ring R] (M : submonoid R) [is_reduced R] :
is_reduced (localization M)
source
theorem is_reduced_of_localization_maximal  :
of_localization_maximal (λ (R : Type u_1) (hR : comm_ring R), is_reduced R)
source
theorem localization_preserves_surjective  :
ring_hom.localization_preserves (λ (R S : Type u_1) (_x : comm_ring R) (_x_1 : comm_ring S) (f : R →+* S), function.surjective ⇑f)
source
theorem surjective_of_localization_span  :
ring_hom.of_localization_span (λ (R S : Type u_1) (_x : comm_ring R) (_x_1 : comm_ring S) (f : R →+* S), function.surjective ⇑f)
source
theorem localization_finite  :
ring_hom.localization_preserves ring_hom.finite

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

source
theorem localization_away_map_finite {R S : Type u} [comm_ring R] [comm_ring S] (R' S' : Type u) [comm_ring R'] [comm_ring S'] (f : R →+* S) [algebra R R'] [algebra S S'] (r : R) [is_localization.away r R'] [is_localization.away (⇑f r) S'] (hf : f.finite) :
(is_localization.away.map R' S' f r).finite
source
theorem is_localization.smul_mem_finset_integer_multiple_span {R S : Type u} [comm_ring R] [comm_ring S] (M : submonoid R) (S' : Type u) [comm_ring S'] [algebra S S'] [algebra R S] [algebra R S'] [is_scalar_tower R S S'] [is_localization (submonoid.map (algebra_map R S) M) S'] (x : S) (s : finset S') (hx : ⇑(algebra_map S S') x ∈ submodule.span R ↑s) :
∃ (m : ↥M), m • x ∈ submodule.span R ↑(is_localization.finset_integer_multiple (submonoid.map (algebra_map R S) M) s)

Let S be an R-algebra, M an 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 finset_integer_multiple _ s over R.

source
theorem multiple_mem_span_of_mem_localization_span {R S : Type u} [comm_ring R] [comm_ring S] (M : submonoid R) (R' : Type u) [comm_ring R'] [algebra R R'] [algebra R' S] [algebra R S] [is_scalar_tower R R' S] [is_localization M R'] (s : set S) (x : S) (hx : x ∈ submodule.span R' s) :
∃ (t : ↥M), t • x ∈ submodule.span R s

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

source
theorem multiple_mem_adjoin_of_mem_localization_adjoin {R S : Type u} [comm_ring R] [comm_ring S] (M : submonoid R) (R' : Type u) [comm_ring R'] [algebra R R'] [algebra R' S] [algebra R S] [is_scalar_tower R R' S] [is_localization 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.

source
theorem finite_of_localization_span  :
ring_hom.of_localization_span ring_hom.finite
source
theorem localization_finite_type  :
ring_hom.localization_preserves ring_hom.finite_type
source
theorem localization_away_map_finite_type {R S : Type u} [comm_ring R] [comm_ring S] (R' S' : Type u) [comm_ring R'] [comm_ring S'] (f : R →+* S) [algebra R R'] [algebra S S'] (r : R) [is_localization.away r R'] [is_localization.away (⇑f r) S'] (hf : f.finite_type) :
(is_localization.away.map R' S' f r).finite_type
source
theorem is_localization.exists_smul_mem_of_mem_adjoin {R S : Type u} [comm_ring R] [comm_ring S] {S' : Type u} [comm_ring S'] [algebra S S'] [algebra R S] [algebra R S'] [is_scalar_tower R S S'] (M : submonoid S) [is_localization M S'] (x : S) (s : finset S') (A : subalgebra R S) (hA₁ : ↑(is_localization.finset_integer_multiple M s) ⊆ ↑A) (hA₂ : M ≤ A.to_submonoid) (hx : ⇑(algebra_map 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.

source
theorem is_localization.lift_mem_adjoin_finset_integer_multiple {R S : Type u} [comm_ring R] [comm_ring S] (M : submonoid R) {S' : Type u} [comm_ring S'] [algebra S S'] [algebra R S] [algebra R S'] [is_scalar_tower R S S'] [is_localization (submonoid.map (algebra_map R S) M) S'] (x : S) (s : finset S') (hx : ⇑(algebra_map S S') x ∈ algebra.adjoin R ↑s) :
∃ (m : ↥M), m • x ∈ algebra.adjoin R ↑(is_localization.finset_integer_multiple (submonoid.map (algebra_map R S) M) s)

Let S be an R-algebra, M an 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 finset_integer_multiple _ s over R.

source
theorem finite_type_of_localization_span  :
ring_hom.of_localization_span ring_hom.finite_type