# mathlibdocumentation

ring_theory.local_properties

# 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 Aₘ for all maximal m.
• P_of_localization_span : P holds for R if given a spanning set {fᵢ}, P holds for all A_{fᵢ}.

## Main results #

The following properties are covered:

• The triviality of an ideal or an element: ideal_eq_zero_of_localization, eq_zero_of_localization
• is_reduced : localization_is_reduced, is_reduced_of_localization_maximal.
• finite: localization_finite, finite_of_localization_span
• finite_type: localization_finite_type, finite_type_of_localization_span
def localization_preserves (P : Π (R : Type u) [_inst_7 : , 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
• = ∀ {R : Type u} [hR : (M : (S : Type u) [hS : [_inst_8 : S] [_inst_9 : S], P RP S
def of_localization_maximal (P : Π (R : Type u) [_inst_7 : , 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
• = ∀ (R : Type u) [_inst_8 : , (∀ (J : ideal R) (hJ : J.is_maximal), P P R
def ring_hom.localization_preserves (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (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
• = ∀ {R S : Type u} [_inst_9 : [_inst_10 : (f : R →+* S) (M : (R' S' : Type u) [_inst_11 : comm_ring R'] [_inst_12 : comm_ring S'] [_inst_13 : R'] [_inst_14 : S'] [_inst_15 : R'] [_inst_16 : S'], P fP f _)
def ring_hom.of_localization_finite_span (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (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
• = ∀ {R S : Type u} [_inst_9 : [_inst_10 : (f : R →+* S) (s : finset R), (∀ (r : s), P r))P f
def ring_hom.of_localization_span (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (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
• = ∀ {R S : Type u} [_inst_9 : [_inst_10 : (f : R →+* S) (s : set R), (∀ (r : s), P r))P f
theorem ring_hom.of_localization_span_iff_finite (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop) :
theorem ring_hom.localization_away_of_localization_preserves {R S : Type u} [comm_ring R] [comm_ring S] {R' S' : Type u} [comm_ring R'] [comm_ring S'] {f : R →+* S} [ R'] [ S'] {P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop} {r : R} [ R'] [ S'] (hf : P f) :
P S' f r)
theorem ideal_eq_zero_of_localization {R : Type u} [comm_ring R] (I : ideal R) (h : ∀ (J : ideal R) (hJ : J.is_maximal), ) :
I = 0

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

theorem eq_zero_of_localization {R : Type u} [comm_ring R] (r : R) (h : ∀ (J : ideal R) (hJ : J.is_maximal), r = 0) :
r = 0
theorem localization_is_reduced  :
localization_preserves (λ (R : Type u_1) (hR : ,
@[protected, instance]
def localization.is_reduced {R : Type u} [comm_ring R] (M : submonoid R) [is_reduced R] :
theorem is_reduced_of_localization_maximal  :
of_localization_maximal (λ (R : Type u_1) (hR : ,

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

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) [ R'] [ S'] (r : R) [ R'] [ S'] (hf : f.finite) :
S' f r).finite
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'] [ S'] [ S] [ S'] [ S'] [is_localization (submonoid.map S) M) S'] (x : S) (s : finset S') (hx : S') x ) :
∃ (m : M), m x

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.

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'] [ R'] [algebra R' S] [ S] [ R' S] [ R'] (s : set S) (x : S) (hx : x s) :
∃ (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 S : Type u} [comm_ring R] [comm_ring S] (M : submonoid R) (R' : Type u) [comm_ring R'] [ R'] [algebra R' S] [ S] [ R' S] [ R'] (s : set S) (x : S) (hx : x s) :
∃ (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_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) [ R'] [ S'] (r : R) [ R'] [ S'] (hf : f.finite_type) :
S' f r).finite_type
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'] [ S'] [ S] [ S'] [ S'] [is_localization (submonoid.map S) M) S'] (x : S) (s : finset S') (hx : S') x ) :
∃ (m : M), m x

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.