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

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

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

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

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

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.