# 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 Rₘ for all maximal m.
• P_of_localization_prime : P holds for R if P holds for Rₘ for all prime m.
• P_of_localization_span : 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_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
def ring_hom.holds_for_localization_away (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (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
• = ∀ ⦃R : Type u⦄ (S : Type u) [_inst_9 : [_inst_10 : [_inst_11 : S] (r : R) [_inst_12 : , P S)
def ring_hom.of_localization_finite_span_target (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_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
def ring_hom.of_localization_span_target (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (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
• = ∀ ⦃R S : Type u⦄ [_inst_9 : [_inst_10 : (f : R →+* S) (s : set S), (∀ (r : s), P ((algebra_map S .comp f))P f
def ring_hom.of_localization_prime (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (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
• = ∀ ⦃R S : Type u⦄ [_inst_9 : [_inst_10 : (f : R →+* S), (∀ (J : ideal S) (hJ : J.is_prime), P f _))P f
structure ring_hom.property_is_local (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop) :
Prop
• localization_preserves :
• of_localization_span_target :
• stable_under_composition :
• holds_for_localization_away :

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 ring_hom.of_localization_span_iff_finite (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop) :
theorem ring_hom.of_localization_span_target_iff_finite (P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop) :
theorem ring_hom.property_is_local.respects_iso {P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop} (hP : ring_hom.property_is_local P) :
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} [ 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 ring_hom.property_is_local.of_localization_span {P : Π {R S : Type u} [_inst_7 : [_inst_8 : , (R →+* S) → Prop} (hP : ring_hom.property_is_local P) :
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 : ,
theorem localization_preserves_surjective  :
ring_hom.localization_preserves (λ (R S : Type u_1) (_x : (_x_1 : (f : R →+* S),
theorem surjective_of_localization_span  :
ring_hom.of_localization_span (λ (R S : Type u_1) (_x : (_x_1 : (f : R →+* S),

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.exists_smul_mem_of_mem_adjoin {R S : Type u} [comm_ring R] [comm_ring S] {S' : Type u} [comm_ring S'] [ S'] [ S] [ S'] [ S'] (M : submonoid S) [ S'] (x : S) (s : finset S') (A : S) (hA₁ : A) (hA₂ : M A.to_submonoid) (hx : S') x ) :
∃ (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 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.