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 forAₘ
for all maximalm
.P_of_localization_span
:P
holds forR
if given a spanning set{fᵢ}
,P
holds for allA_{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
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
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
.