Ideal.eq_of_localization_maximal
theorem Ideal.eq_of_localization_maximal :
∀ {R : Type u} [inst : CommRing R] {I J : Ideal R},
(∀ (P : Ideal R) (x : P.IsMaximal),
Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) J) →
I = J
The theorem `Ideal.eq_of_localization_maximal` states that for a commutative ring `R` and two ideals `I` and `J` of `R`, if, for every maximal ideal `P` of `R`, the localization of `I` at `P` is equal to the localization of `J` at `P`, then `I` equals `J`. Here, localization is performed using the ring homomorphism given by the algebra structure from `R` to the localization of `R` at the complement of `P`.
More concisely: If two ideals `I` and `J` of a commutative ring `R` have equal localizations at every maximal ideal `P` of `R`, then `I = J`.
|
IsLocalization.lift_mem_adjoin_finsetIntegerMultiple
theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple :
∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (M : Submonoid R) {S' : Type u} [inst_2 : CommRing S']
[inst_3 : Algebra S S'] [inst_4 : Algebra R S] [inst_5 : Algebra R S'] [inst_6 : IsScalarTower R S S']
[inst_7 : IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S'),
(algebraMap S S') x ∈ Algebra.adjoin R ↑s →
∃ m, m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
The theorem `IsLocalization.lift_mem_adjoin_finsetIntegerMultiple` states that given a commutative ring `R`, a commutative ring `S` that is an `R`-algebra, a submonoid `M` of `R`, a commutative ring `S'` which is the localization of `S` at `M`, and an element `x` of `S`, if the image of `x` under the mapping from `S` to `S'` falls in the subalgebra of `R` spanned by a finite subset `s` of `S'`, then there exists an element `m` in `M` such that `m` times `x` falls in the subalgebra of `R` spanned by the set of all numerators obtained after clearing the denominators of the elements of `s` in the localization of `S` at `M`. This theorem is a statement about the interaction between localization at a submonoid, scalar multiplication, and the generation of subalgebras.
More concisely: Given a commutative ring R, an R-algebra S, a submonoid M of R, the localization S' of S at M, and an element x in S, if x maps to an element in the subalgebra of R generated by a finite subset of S' and images of S under localization, then there exists m in M such that mx is in the subalgebra of R generated by the numerators of elements in that subset after localization.
|
ideal_eq_bot_of_localization'
theorem ideal_eq_bot_of_localization' :
∀ {R : Type u} [inst : CommRing R] (I : Ideal R),
(∀ (J : Ideal R) (hJ : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) → I = ⊥
This theorem states that for any ideal `I` in a commutative ring `R`, if the image of `I` under the map induced by the canonical embedding `algebraMap` of `R` into the localization of `R` at every maximal ideal `J` is the zero ideal (denoted by ⊥), then `I` itself must be the zero ideal. In other words, an ideal is trivial (i.e., the zero ideal) if its localization at every maximal ideal is also trivial.
More concisely: If the localization of an ideal at every maximal ideal is the zero ideal in a commutative ring, then the ideal is the zero ideal.
|
ideal_eq_bot_of_localization
theorem ideal_eq_bot_of_localization :
∀ {R : Type u} [inst : CommRing R] (I : Ideal R),
(∀ (J : Ideal R) (hJ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥) → I = ⊥
This theorem states that for any commutative ring `R` and any ideal `I` of `R`, if the localization of `I` at all maximal ideals `J` of `R` results in the bottom (or trivial) ideal, then `I` itself must be the bottom ideal. In other words, if when we localize an ideal at every maximal ideal we always get the trivial ideal, then the original ideal was trivial to begin with. This theorem allows us to characterize the triviality of an ideal in terms of its localizations at maximal ideals.
More concisely: If the localization of an ideal in a commutative ring at every maximal ideal is the bottom ideal, then the original ideal is the bottom ideal.
|
Ideal.le_of_localization_maximal
theorem Ideal.le_of_localization_maximal :
∀ {R : Type u} [inst : CommRing R] {I J : Ideal R},
(∀ (P : Ideal R) (hP : P.IsMaximal),
Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ Ideal.map (algebraMap R (Localization.AtPrime P)) J) →
I ≤ J
This theorem states that for any commutative ring `R` and any two ideals `I` and `J` of `R`, if for every maximal ideal `P` of `R`, the image of `I` under the localization map at `P` is contained within the image of `J` under the same map, then `I` is a subset of `J`. In other words, the theorem provides a criterion for comparing ideals based on their behaviors under localizations at maximal ideals.
More concisely: If for every maximal ideal `P` of a commutative ring `R`, the localization of `I` at `P` is contained in the localization of `J` at `P`, then `I` is contained in `J`.
|
IsLocalization.smul_mem_finsetIntegerMultiple_span
theorem IsLocalization.smul_mem_finsetIntegerMultiple_span :
∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (M : Submonoid R) (S' : Type u) [inst_2 : CommRing S']
[inst_3 : Algebra S S'] [inst_4 : Algebra R S] [inst_5 : Algebra R S'] [inst_6 : IsScalarTower R S S']
[inst_7 : IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S'),
(algebraMap S S') x ∈ Submodule.span R ↑s →
∃ m, m • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
The theorem "IsLocalization.smul_mem_finsetIntegerMultiple_span" states that given an `R`-algebra `S`, a submonoid `M` of `R`, and `S'` defined as `M⁻¹S` (the localization of `S` at `M`), if the image of some element `x` from `S` under the algebra homomorphism to `S'` falls in the span of a finite subset `s` of `S'` over `R`, then there exists some element `m` in `M` such that the scalar multiplication `m • x` falls in the span of the set of numerators obtained after clearing the denominators of `s` over `R`, where the set of numerators is computed using the "IsLocalization.finsetIntegerMultiple" function.
In other words, we can find an integer multiple of `x` that lies in the span of the integer multiples of the elements of `s`. The span is defined as the smallest submodule that contains the given set.
More concisely: Given an `R`-algebra `S`, an `R`-submonoid `M`, and `S' = M^(-1)S`, if an element `x` in `S` lies in the span of a finite subset `s` in `S'` over `R`, then there exists an `m` in `M` such that `m • x` is in the span of the numerators of `s` over `R`.
|
localization_finite
theorem localization_finite : RingHom.LocalizationPreserves @RingHom.Finite
The theorem `localization_finite` states that if `S` is a finite `R`-algebra, then the localization of `S` at a multiplicative set `M`, denoted as `S' = M⁻¹S`, is a finite algebra over the localization of `R` at the same set `M`, denoted as `R' = M⁻¹R`. In other words, the property of being a finite algebra is preserved under the process of localization.
More concisely: If `S` is a finite `R`-algebra, then the localization `M⁻¹S` of `S` at a multiplicative set `M` is a finite `R' = M⁻¹R`-algebra.
|
multiple_mem_adjoin_of_mem_localization_adjoin
theorem multiple_mem_adjoin_of_mem_localization_adjoin :
∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (M : Submonoid R) (R' : Type u) [inst_2 : CommRing R']
[inst_3 : Algebra R R'] [inst_4 : Algebra R' S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R R' S]
[inst_7 : IsLocalization M R'] (s : Set S), ∀ x ∈ Algebra.adjoin R' s, ∃ t, t • x ∈ Algebra.adjoin R s
This theorem states that given a commutative ring `R`, a submonoid `M` of `R`, and an `R'` algebra `S` where `R'` is the localization of `R` at `M`, if a certain element `x` belongs to the 'adjoin' of `R'` and a set `s`, then there exists an element `t` in `M` such that the scalar multiplication of `t` and `x` belongs to the 'adjoin' of `R` and the set `s`. The 'adjoin' operation is the construction of the smallest subalgebra that contains a given set.
More concisely: Given a commutative ring `R`, a submonoid `M` of `R`, an `R'`-algebra `S` over the localization of `R` at `M`, and `x` in the adjoin of `R'` and a set `s`, there exists `t` in `M` such that `tx` is in the adjoin of `R` and `s`.
|
multiple_mem_span_of_mem_localization_span
theorem multiple_mem_span_of_mem_localization_span :
∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (M : Submonoid R) (R' : Type u) [inst_2 : CommRing R']
[inst_3 : Algebra R R'] [inst_4 : Algebra R' S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R R' S]
[inst_7 : IsLocalization M R'] (s : Set S), ∀ x ∈ Submodule.span R' s, ∃ t, t • x ∈ Submodule.span R s
This theorem states that if `S` is an algebra over `R' = M⁻¹R`, where `M` is a submonoid of `R`, and if a given element `x` belongs to the span of a set `s` with coefficients in `R'`, then there exists some element `t` in `M` such that `t` times `x` belongs to the span of `s` with coefficients in `R`. This essentially means that if `x` is a linear combination of elements in `s` using coefficients from the localization `R'`, then `x` can also be obtained as a linear combination of elements in `s` using coefficients from `R` after multiplication by a suitable element from the submonoid `M`. This theorem is a part of the theory of localization of rings and modules.
More concisely: If `x` is in the span of a set `s` over the localization `R'` of ring `R` with respect to a submonoid `M`, then there exists an element `t` in `M` such that `tx` is in the span of `s` over `R`.
|
IsLocalization.exists_smul_mem_of_mem_adjoin
theorem IsLocalization.exists_smul_mem_of_mem_adjoin :
∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {S' : Type u} [inst_2 : CommRing S']
[inst_3 : Algebra S S'] [inst_4 : Algebra R S] [inst_5 : Algebra R S'] [inst_6 : IsScalarTower R S S']
(M : Submonoid S) [inst_7 : IsLocalization M S'] (x : S) (s : Finset S') (A : Subalgebra R S),
↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A →
M ≤ A.toSubmonoid → (algebraMap S S') x ∈ Algebra.adjoin R ↑s → ∃ m, m • x ∈ A
This theorem states that given an `R`-algebra `S`, a submonoid `M` of `S`, and a localization `S'` of `S` at `M`, if the image of an element `x` from `S` under the algebra map to `S'` lies within the subalgebra generated over `R` by a finite subset `s` of `S'` (denoted as the `Algebra.adjoin` of `s`), and if `A` is an `R`-subalgebra of `S` that contains both `M` and the numerators of `s` (obtained by the function `IsLocalization.finsetIntegerMultiple`), then there exists an element `m` from `M` such that the scalar multiplication of `m` and `x` is an element of `A`. Intuitively, it's saying that if `A` contains certain elements and their numerators, and if `x` maps into a special subalgebra associated with these elements, then a scaled version of `x` lands in `A`.
More concisely: Given an `R`-algebra `S`, a submonoid `M` of `S`, and a localization `S'` of `S` at `M`, if for some finite subset `s` of `S'`, the image of an element `x` from `S` under the algebra map to `S'` lies in the subalgebra generated by `s` over `R`, and `A` is an `R`-subalgebra containing both `M` and the numerators of `s`, then there exists `m` in `M` such that `mx` is in `A`.
|
Module.Finite_of_isLocalization
theorem Module.Finite_of_isLocalization :
∀ (R : Type u_1) (S : Type u_2) (Rₚ : Type u_3) (Sₚ : Type u_4) [inst : CommSemiring R] [inst_1 : CommRing S]
[inst_2 : CommRing Rₚ] [inst_3 : CommRing Sₚ] [inst_4 : Algebra R S] [inst_5 : Algebra R Rₚ]
[inst_6 : Algebra R Sₚ] [inst_7 : Algebra S Sₚ] [inst_8 : Algebra Rₚ Sₚ] [inst_9 : IsScalarTower R S Sₚ]
[inst_10 : IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [inst_11 : IsLocalization M Rₚ]
[inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S], Module.Finite Rₚ Sₚ
The theorem `Module.Finite_of_isLocalization` states that, given commutative semirings `R` and `S`, commutative rings `Rₚ` and `Sₚ`, and algebras of `R` over `S`, `Rₚ`, `Sₚ`, combined with the scalar towers `R` over `S` over `Sₚ` and `R` over `Rₚ` over `Sₚ`, and given a submonoid `M` of `R`, if `Rₚ` is a localization of `R` at `M`, and `Sₚ` is a localization of `S` at the image of `M` under the algebra map from `R` to `S`, and if `S` is a finite module over `R`, then `Sₚ` is also a finite module over `Rₚ`. This theorem is essentially a statement about the preservation of "finiteness" property under the localization process in the context of rings and modules.
More concisely: Given commutative rings R and S, semirings Rₚ and Sₚ, algebras Rₚ over S, Sₚ over Rₚ, and scalar towers R over S and R over Rₚ over S, if Rₚ is a localization of R at a submonoid M and Sₚ is a localization of S at M's image under the algebra map, and S is finite over R, then Sₚ is finite over Rₚ.
|