IsLocalization.localization_isScalarTower_of_submonoid_le
theorem IsLocalization.localization_isScalarTower_of_submonoid_le :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
(T : Type u_4) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (M N : Submonoid R) (h : M ≤ N)
[inst_5 : IsLocalization M S] [inst_6 : IsLocalization N T], IsScalarTower R S T
This theorem states that for any commutative semiring `R` and any two submonoids `M` and `N` of `R` such that `M` is a subset of `N`, if `S` is the localization of `R` at `M` and `T` is the localization of `R` at `N`, then the scalar multiplication operation in `R` commutes with the mappings from `S` and `T`. This is expressed as a property known as 'scalar tower', denoted as `IsScalarTower R S T`, where if `R` is a semiring and `S` and `T` are `R`-algebras, then scalar multiplication in `R`, `S`, and `T` is associative.
More concisely: For any commutative semiring R, if M and N are submonoids of R with M a subset of N, and S and T are the localizations of R at M and N respectively, then scalar multiplication in R commutes with the structure maps from S to T (scalar tower property).
|
IsFractionRing.isFractionRing_of_isLocalization
theorem IsFractionRing.isFractionRing_of_isLocalization :
∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_3) (T : Type u_4) [inst_1 : CommRing S]
[inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
[inst_6 : IsScalarTower R S T] [inst_7 : IsLocalization M S] [inst_8 : IsFractionRing R T],
M ≤ nonZeroDivisors R → IsFractionRing S T
This theorem states that if we have two commutative rings `R` and `S`, and a submonoid `M` of `R`, such that `S` is a localization of `R` at `M`, and we also have a third commutative ring `T` such that `T` is the field of fractions of `R`, with an algebra structure defined between `R`, `S`, and `T` and the additional condition that `R`, `S`, `T` form a scalar tower. If `M` is a subset of the non-zero divisors of `R`, then `T` is also the field of fractions of `S`. In simpler terms, we can carry the fraction field structure from `R` to `S` through localization, given that the localization does not introduce zero divisors.
More concisely: If `R` and `S` are commutative rings with `S` being a localization of `R` at a submonoid `M` of non-zero divisors in `R`, and if `T` is the field of fractions of `R` with an algebra structure making `R`, `S`, and `T` a scalar tower, then `T` is the field of fractions of `S`.
|
IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
theorem IsLocalization.isLocalization_isLocalization_atPrime_isLocalization :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] (T : Type u_4) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
[inst_6 : IsScalarTower R S T] [inst_7 : IsLocalization M S] (p : Ideal S) [Hp : p.IsPrime]
[inst_8 : IsLocalization.AtPrime T p], IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)
This theorem states that for any commutative semiring `R` with a submonoid `M`, and any other commutative semirings `S` and `T` that act as `R`-algebras, if `S` is the localization of `R` at `M`, and `p` is a prime ideal of `S`, then the semiring `T` is the localization of `R` at the preimage of `p` under the localization map from `R` to `S`, provided that `T` is also the localization of `S` at `p` and forms a scalar tower with `R` and `S`. In other words, localization at a prime ideal in the localization ring corresponds to localization at the preimage of that ideal in the original ring.
More concisely: For any commutative semirings `R`, `S`, and `T`, if `R` is the base ring, `M` is a submonoid of `R`, `S` is the localization of `R` at `M`, `T` is the localization of both `S` and `R` at a common prime ideal, and `T` forms a scalar tower with `R` and `S`, then the ideal in `R` mapping to the given prime ideal in `S` is the preimage of the prime ideal in `R` under the localization map.
|
IsLocalization.isLocalization_of_is_exists_mul_mem
theorem IsLocalization.isLocalization_of_is_exists_mul_mem :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
(M N : Submonoid R) [inst_3 : IsLocalization M S], M ≤ N → (∀ (x : ↥N), ∃ m, m * ↑x ∈ M) → IsLocalization N S
The theorem `IsLocalization.isLocalization_of_is_exists_mul_mem` asserts that for any commutative semiring `R` and its algebra `S`, and any two submonoids `M` and `N` of `R` such that `M` is contained in `N` and for every element `x` of `N` there exists an element `m` of `R` such that the multiplication of `m` and `x` is in `M`, then the localization of `R` at `N` is the same as the localization of `R` at `M`. In mathematical terms, if `M ≤ N` are submonoids of a ring `R` and for all `x` in `N`, there exists `m` in `R` such that `m * x` is in `M`, then the localization of `R` at `N` is equal to the localization of `R` at `M`.
More concisely: If `M` is a submonoid of `N` in a commutative semiring `R` such that every `x` in `N` has an `m` in `R` with `m * x` in `M`, then the localizations of `R` at `M` and `N` are equal.
|
IsLocalization.localization_localization_isLocalization_of_has_all_units
theorem IsLocalization.localization_localization_isLocalization_of_has_all_units :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] (N : Submonoid S) (T : Type u_4) [inst_3 : CommSemiring T] [inst_4 : Algebra R T]
[inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] [inst_7 : IsLocalization M S] [inst_8 : IsLocalization N T],
(∀ (x : S), IsUnit x → x ∈ N) → IsLocalization (Submonoid.comap (algebraMap R S) N) T
This theorem states that given a commutative semiring `R` with a submonoid `M`, and a commutative semiring `S` which is a localization of `R` at `M` with a submonoid `N`, and a commutative semiring `T` which is a localization of `S` at `N`, if `N` contains all units of `S`, then `T` is a localization of `R` at the preimage of `N` under the map from `R` to `S`. This illustrates the concept of localization of a localization being a localization.
More concisely: Given commutative semirings `R`, `S`, and `T`, if `R` is locally localized to `S` at a submonoid `M` and `S` is locally localized to `T` at a submonoid `N` containing all units of `S`, then `T` is the localization of `R` at the preimage of `N` under the map from `R` to `S`.
|
IsLocalization.isLocalization_of_submonoid_le
theorem IsLocalization.isLocalization_of_submonoid_le :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
(T : Type u_4) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (M N : Submonoid R),
M ≤ N →
∀ [inst_5 : IsLocalization M S] [inst_6 : IsLocalization N T] [inst_7 : Algebra S T]
[inst_8 : IsScalarTower R S T], IsLocalization (Submonoid.map (algebraMap R S) N) T
This theorem states that given two submonoids `M` and `N` of a commutative semiring `R` such that `M` is a subset of `N`, and given two algebras `S` and `T` over `R` such that `S` is a localization of `R` at `M` and `T` is a localization of `R` at `N`, if there is an algebra structure from `S` to `T` and `T` is also an algebra over `R` under a scalar tower, then `T` is also a localization of `S` at the image of `N` under the algebra map from `R` to `S`. In essence, this theorem allows us to "lift" localizations from `R` to `S`.
More concisely: Given commutative semirings R, submonoids M ⊆ N, localizations S = R\_[M] and T = R\_[N], an algebra structure from S to T, and T being an R-algebra under a scalar tower, then T is a localization of S at the image of N under the algebra map from R to S.
|
IsLocalization.localization_localization_isLocalization
theorem IsLocalization.localization_localization_isLocalization :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] (N : Submonoid S) (T : Type u_4) [inst_3 : CommSemiring T] [inst_4 : Algebra R T]
[inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] [inst_7 : IsLocalization M S] [inst_8 : IsLocalization N T],
IsLocalization (IsLocalization.localizationLocalizationSubmodule M N) T
This theorem states that, given two submodules `M` and `N` of the commutative semirings `R` and `S` respectively, with `S` being the localization of `R` with respect to `M` and `f` being the localization map from `R` to `S`, the set `N⁻¹S` which is the localization of `S` with respect to `N`, is equal to the ring `T`, which we can also represent as `(f⁻¹ (N • f(M)))⁻¹ R`, the localization of `R` with respect to the preimage of the product of `N` and the image of `M` under `f`. This essentially means that the localization of a localization is itself a localization. The context requires `R`, `S` and `T` to be commutative semirings, `S` and `T` to be algebra over `R`, and `T` also to be an algebra over `S` with `R`, `S` and `T` forming a scalar tower. Also, `S` must be a localization of `R` with respect to `M` and `T` must be a localization of `S` with respect to `N`.
More concisely: Given commutative semirings R, S, and T with S being a localization of R with respect to a submodule M, and T being a localization of S with respect to a submodule N, the localization of S with respect to N is equal to the localization of R with respect to the preimage of N under the localization map from R to S and the image of M under the same map.
|