mathlib documentation

ring_theory.local_properties

Local properties of commutative rings #

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

Naming Conventions #

Main results #

The following properties are covered:

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
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
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
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
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
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) :
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} [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) :
theorem ideal_eq_zero_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 = 0) :
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), (algebra_map R (localization.at_prime J)) r = 0) :
r = 0
theorem localization_is_reduced  :
localization_preserves (λ (R : Type u_1) (hR : comm_ring R), is_reduced R)
@[protected, instance]

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) [algebra R R'] [algebra S S'] (r : R) [is_localization.away r R'] [is_localization.away (f r) S'] (hf : f.finite) :

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'] [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.

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.

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

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.