Local properties of commutative rings #
In this file, we provide the proofs of various local properties.
Naming Conventions #
localization_P
:P
holds forS⁻¹R
ifP
holds forR
.P_of_localization_maximal
:P
holds forR
ifP
holds forRₘ
for all maximalm
.P_of_localization_prime
:P
holds forR
ifP
holds forRₘ
for all primem
.P_of_localization_span
:P
holds forR
if given a spanning set{fᵢ}
,P
holds for allR_{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
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
- localization_preserves P = ∀ {R : Type u} [hR : comm_ring R] (M : submonoid R) (S : Type u) [hS : comm_ring S] [_inst_8 : algebra R S] [_inst_9 : is_localization M S], P R → P S
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
- of_localization_maximal P = ∀ (R : Type u) [_inst_8 : comm_ring R], (∀ (J : ideal R) (hJ : J.is_maximal), P (localization.at_prime J)) → P R
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
- ring_hom.localization_preserves P = ∀ ⦃R S : Type u⦄ [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] (f : R →+* S) (M : submonoid R) (R' S' : Type u) [_inst_11 : comm_ring R'] [_inst_12 : comm_ring S'] [_inst_13 : algebra R R'] [_inst_14 : algebra S S'] [_inst_15 : is_localization M R'] [_inst_16 : is_localization (submonoid.map f M) S'], P f → P (is_localization.map S' f _)
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
- ring_hom.of_localization_finite_span P = ∀ ⦃R S : Type u⦄ [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] (f : R →+* S) (s : finset R), ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (localization.away_map f ↑r)) → P f
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
- ring_hom.of_localization_span P = ∀ ⦃R S : Type u⦄ [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] (f : R →+* S) (s : set R), ideal.span s = ⊤ → (∀ (r : ↥s), P (localization.away_map f ↑r)) → P f
A property P
of ring homs satisfies ring_hom.holds_for_localization_away
if P
holds for each localization map R →+* Rᵣ
.
Equations
- ring_hom.holds_for_localization_away P = ∀ ⦃R : Type u⦄ (S : Type u) [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] [_inst_11 : algebra R S] (r : R) [_inst_12 : is_localization.away r S], P (algebra_map R S)
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
- ring_hom.of_localization_finite_span_target P = ∀ ⦃R S : Type u⦄ [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] (f : R →+* S) (s : finset S), ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebra_map S (localization.away ↑r)).comp f)) → P f
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
- ring_hom.of_localization_span_target P = ∀ ⦃R S : Type u⦄ [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] (f : R →+* S) (s : set S), ideal.span s = ⊤ → (∀ (r : ↥s), P ((algebra_map S (localization.away ↑r)).comp f)) → P f
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
- ring_hom.of_localization_prime P = ∀ ⦃R S : Type u⦄ [_inst_9 : comm_ring R] [_inst_10 : comm_ring S] (f : R →+* S), (∀ (J : ideal S) (hJ : J.is_prime), P (localization.local_ring_hom (ideal.comap f J) J f _)) → P f
- localization_preserves : ring_hom.localization_preserves P
- of_localization_span_target : ring_hom.of_localization_span_target P
- stable_under_composition : ring_hom.stable_under_composition P
- holds_for_localization_away : ring_hom.holds_for_localization_away P
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ᵣ)
.
An ideal is trivial if its localization at every maximal ideal is trivial.
If S
is a finite R
-algebra, then S' = M⁻¹S
is a finite R' = M⁻¹R
-algebra.
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
.
If S
is an R' = M⁻¹R
algebra, and x ∈ span R' s
,
then t • x ∈ span R s
for some t : M
.
If S
is an R' = M⁻¹R
algebra, and x ∈ adjoin R' s
,
then t • x ∈ adjoin R s
for some t : M
.
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
.
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
.