IsLocalization.map_comp_map
theorem IsLocalization.map_comp_map :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
{T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] (hy : M ≤ Submonoid.comap g T) [inst_6 : Algebra P Q]
[inst_7 : IsLocalization T Q] {A : Type u_5} [inst_8 : CommSemiring A] {U : Submonoid A} {W : Type u_6}
[inst_9 : CommSemiring W] [inst_10 : Algebra A W] [inst_11 : IsLocalization U W] {l : P →+* A}
(hl : T ≤ Submonoid.comap l U),
(IsLocalization.map W l hl).comp (IsLocalization.map Q g hy) = IsLocalization.map W (l.comp g) ⋯
The theorem `IsLocalization.map_comp_map` states that, in the context of commutative semirings, if we have homomorphisms `g` from `R` to `P` and `l` from `P` to `A` that can induce maps of localizations, then the composition of the induced maps is equal to the map of localizations induced by the composition `l ∘ g`. Here, `R`, `P`, `A` are commutative semirings, `M` and `T` are submonoids of `R` and `P` respectively, `S`, `Q`, `W` are the localizations of `R`, `P`, `A` at `M`, `T`, `U` respectively, and `U` is a submonoid of `A`. The condition `hy : M ≤ Submonoid.comap g T` ensures that the image of `M` under `g` is contained in `T`, and similarly for `hl : T ≤ Submonoid.comap l U`.
More concisely: Given commutative semirings R, P, A, submonoids M of R, T of P, and U of A, if g : R -> P and l : P -> A are homomorphisms inducing localization maps, and M is contained in the image of g under the submonoid composition with T, and T is contained in the image of l under the submonoid composition with U, then the localization maps induced by g and l followed by their compositions equal the localization map induced by the composition of g and l.
|
localizationAlgebra_injective
theorem localizationAlgebra_injective :
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
(Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
[inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ],
Function.Injective ⇑(algebraMap R S) → Function.Injective ⇑(algebraMap Rₘ Sₘ)
This theorem states that if the algebra map from a commutative ring `R` to another commutative ring `S` is injective (meaning no two distinct elements of `R` map to the same element of `S`), then the same injectivity property holds for the algebra maps from the localizations `Rₘ` and `Sₘ` of `R` and `S` at submonoids `M` and `Algebra.algebraMapSubmonoid S M`, respectively. In more informal terms, if no "information" is lost when mapping from `R` to `S`, then no "information" is lost either when mapping from the localizations `Rₘ` to `Sₘ`.
More concisely: If `f : R → S` is an injective algebra homomorphism between commutative rings `R` and `S`, then the localizations `fⁱ : Rₘ → Sₘ` at any submonoids `M ⊆ R` and `Algebra.algebraMapSubmonoid S Algebra.toSubmonoid xs` (where `xs : set S`) are also injective.
|
IsLocalization.algebraMap_apply_eq_map_map_submonoid
theorem IsLocalization.algebraMap_apply_eq_map_map_submonoid :
∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
(Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
[inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ] [inst_10 : IsScalarTower R Rₘ Sₘ]
[inst_11 : IsScalarTower R S Sₘ] (x : Rₘ), (algebraMap Rₘ Sₘ) x = (IsLocalization.map Sₘ (algebraMap R S) ⋯) x
This theorem states that for a commutative ring `R` with a submonoid `M`, and its localization `Rₘ`, along with a commutative ring `S` and its localization `Sₘ`, if there are algebra structures from `R` to `S`, `R` to `Rₘ`, `S` to `Sₘ`, `Rₘ` to `Sₘ`, and `R` to `Sₘ`; scalar towers from `R` to `Rₘ` to `Sₘ`, and from `R` to `S` to `Sₘ`; and the localization of `M` at `Rₘ` and the submonoid map from `S` to `M` at `Sₘ`, then for any element `x` in `Rₘ`, the result of applying the algebra map from `Rₘ` to `Sₘ` to `x` is the same as applying the localization map from `Rₘ` to `Sₘ` with respect to the algebra map from `R` to `S` to `x`. The theorem is essentially stating the commutativity of the diagram with respect to the algebra map and the localization map for the given settings.
More concisely: Given commutative rings `R` and `S`, their localizations `Rₘ` and `Sₘ`, a submonoid `M` of `R`, algebra structures and scalar towers as specified, the localization of `M` at `Rₘ` and the submonoid map from `S` to `M` at `Sₘ`, then for any `x` in `Rₘ`, the algebra map from `Rₘ` to `Sₘ` applied to `x` equals the localization map from `Rₘ` to `Sₘ` with respect to the algebra map from `R` to `S` applied to `x`.
|
IsLocalization.map_units
theorem IsLocalization.map_units :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (y : ↥M), IsUnit ((algebraMap R S) ↑y)
This theorem states that for any commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S` and a localization `S` of `M`, every element `y` of the submonoid `M` becomes a unit when mapped into `S` using the algebra mapping. In other words, every `y` in `M` has a multiplicative inverse in the image of `algebraMap` from `R` to `S`. This is an important property in the study of localizations in algebraic structures.
More concisely: For any commutative semiring `R`, submonoid `M` of `R`, commutative semiring `S` with `M` as a local subsemigroup, the algebra map from `R` to `S` maps each element `y` in `M` to an element with a multiplicative inverse in `S`.
|
IsLocalization.noZeroDivisors_of_le_nonZeroDivisors
theorem IsLocalization.noZeroDivisors_of_le_nonZeroDivisors :
∀ {S : Type u_2} [inst : CommRing S] (A : Type u_6) [inst_1 : CommRing A] [inst_2 : IsDomain A]
[inst_3 : Algebra A S] {M : Submonoid A} [inst_4 : IsLocalization M S],
M ≤ nonZeroDivisors A → NoZeroDivisors S
The theorem `IsLocalization.noZeroDivisors_of_le_nonZeroDivisors` states that if we have a commutative ring `S`, which is the localization of a ring `A` without zero divisors at a subset of non-zero elements, and if the multiplicative submonoid `M` of `A` is a subset of the non-zero divisors of `A`, then `S` does not have zero divisors. In other words, localization at a subset of non-zero elements preserves the property of having no zero divisors. This is important as it ensures that operations in the localized ring `S` won't unexpectedly result in zero, provided the original ring `A` did not contain zero divisors and the elements we localized at were also non-zero divisors.
More concisely: If a commutative ring is obtained by localizing a submonoid of non-zero divisors of a ring without zero divisors, then the resulting ring has no zero divisors.
|
IsLocalization.sec_spec
theorem IsLocalization.sec_spec :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
z * (algebraMap R S) ↑(IsLocalization.sec M z).2 = (algebraMap R S) (IsLocalization.sec M z).1
The theorem `IsLocalization.sec_spec` states that for any element `z` of type `S`, under the conditions of `R` being a commutative semiring, `M` being a submonoid of `R`, `S` being a commutative semiring and an algebra over `R`, and `S` being a localization of `R` at `M`, the result of applying the section function `IsLocalization.sec` on `z` gives us a pair `(x, y)` of type `R × M` such that the multiplication of `z` and the algebraic mapping of `y` to `S` equals the algebraic mapping of `x` to `S`. In algebraic terms, this can be denoted as `z * f(y) = f(x)`, where `f` is the algebraic map from `R` to `S`. This lemma is true by virtue of the definition of the section function `IsLocalization.sec`.
More concisely: Given a commutative semiring R, a submonoid M of R, an algebra S over R, and under the conditions that R is a localization of S at M, for any element z in S, there exists a pair (x, y) in R × M such that z * f(y) = f(x) holds, where f is the algebraic map from R to S.
|
IsLocalization.sec_spec'
theorem IsLocalization.sec_spec' :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
(algebraMap R S) (IsLocalization.sec M z).1 = (algebraMap R S) ↑(IsLocalization.sec M z).2 * z
This theorem states that given a commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S`, an algebra structure from `R` to `S`, and a localization `S` of `R` at `M`, for any element `z` in `S`, the application of the algebra map to the first element of the pair `(x, y)` returned by the `IsLocalization.sec` function applied to `z` is equal to the product of `z` and the algebra map applied to the second element of the pair `(x, y)`. Here, `(x, y)` is a pair in `R × M` such that `z * f y = f x`. This theorem is essentially an application of the commutativity of `S`.
More concisely: Given a commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S`, an algebra homomorphism `f : R → S`, and a localization `S` of `R` at `M`, for any `z` in `S` and `(x, y)` in `R × M` with `z * f y = f x`, we have `f(x) * z = f(x * y)`.
|
IsLocalization.mk'_surjective
theorem IsLocalization.mk'_surjective :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S), ∃ x y, IsLocalization.mk' S x y = z
The theorem `IsLocalization.mk'_surjective` states that for any commutative semiring `R`, any submonoid `M` of `R`, and any commutative semiring `S` that is a localization of `R` at `M`, and for any element `z` of `S`, there exist an element `x` in `R` and an element `y` in `M` such that the image of `(x, y)` under the surjection `IsLocalization.mk'` is `z`. In other words, every element of `S` can be written as "a (image of `x` under the canonical map) times the inverse of (an image of `y` under the canonical map)", where `x` comes from `R` and `y` comes from `M`.
More concisely: For any commutative semirings R, any submonoid M of R, and any localization S of R at M, every element z in S can be written as x/y for some x in R and y in M, where the division is performed in S using the canonical maps.
|
IsLocalization.exists_of_eq
theorem IsLocalization.exists_of_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [self : IsLocalization M S] {x y : R},
(algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
This theorem states that for any commutative semiring `R`, a submonoid `M` of `R`, a type `S` which is also a commutative semiring and an algebra over `R`, and given that `S` is a localization of `M`, if `x` and `y` are elements of `R` such that their images under the algebra map from `R` to `S` are equal, then there exists an element `c` in `M` such that `c` times `x` is equal to `c` times `y`. This essentially says that if `x` and `y` map to the same element in the algebra `S`, then they must be multiples of the same element from the submonoid `M`.
More concisely: Given a commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S` that is a localization of `M`, and an algebra homomorphism from `R` to `S`, if `x` and `y` in `R` map to the same element in `S`, then there exists `c` in `M` such that `cx = cy`.
|
IsLocalization.injective
theorem IsLocalization.injective :
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
[inst_3 : IsLocalization M S], M ≤ nonZeroDivisors R → Function.Injective ⇑(algebraMap R S)
This theorem states that for any commutative ring `R`, a submonoid `M` of `R`, a type `S` which is also a commutative ring and an algebra over `R`, and given that `S` is a localization of `R` at `M`, if `M` is a subset of the non-zero divisors of `R`, then the algebra homomorphism from `R` to `S` (given by the `Algebra` structure) is injective. In other words, if every element of the submonoid `M` is a non-zero divisor in `R`, then no two distinct elements in `R` have the same image in `S` under the algebra map.
More concisely: If `R` is a commutative ring, `M` is a commutative submonoid of non-zero divisors in `R`, `S` is a commutative ring and an `R`-algebra that is a localization of `R` at `M`, then the algebra homomorphism from `R` to `S` is injective.
|
IsLocalization.subsingleton
theorem IsLocalization.subsingleton :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S], 0 ∈ M → Subsingleton S
The theorem `IsLocalization.subsingleton` states that given a type `R` with a commutative, associative ring structure, a subset `M` of `R` constituting a submonoid, and a type `S` with a commutative, associative ring structure that forms an algebra over `R` and is a localization at `M`, if the submonoid `M` contains the element `0`, then `S` is a subsingleton. In other words, if `0` is an element of the submonoid used for localization, then the localization ring contains at most one element.
More concisely: If `R` is a commutative associative ring, `M` is a submonoid of `R` containing `0`, and `S` is the localization of `R` at `M`, then `S` is a subsingleton.
|
IsLocalization.ringEquivOfRingEquiv.proof_5
theorem IsLocalization.ringEquivOfRingEquiv.proof_5 :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {P : Type u_2} [inst_1 : CommSemiring P]
{T : Submonoid P} (h : R ≃+* P), Submonoid.map h.toMonoidHom M = T → M ≤ Submonoid.comap (↑h) T
This theorem states that for any commutative semirings `R` and `P` with submonoids `M` and `T` respectively, and a given ring equivalence `h` from `R` to `P`, if the image of submonoid `M` under the monoid homomorphism induced by `h` is equal to `T`, then `M` is a subset of the preimage of `T` under the inverse of the monoid homomorphism induced by `h`. This is essentially saying that the preimage of `T` contains `M` when `M` is mapped to `T` by the ring equivalence `h`.
More concisely: If `h` is a ring equivalence from commutative semirings `R` to `P` with submonoids `M` in `R` and `T` in `P`, such that the image of `M` under the monoid homomorphism induced by `h` equals `T`, then `M` is a subset of the preimage of `T` under the inverse monoid homomorphism of `h`.
|
Localization.mk_eq_mk'
theorem Localization.mk_eq_mk' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R}, Localization.mk = IsLocalization.mk' (Localization M)
This theorem states that for any commutative semiring `R` and any submonoid `M` of `R`, the function `Localization.mk` is equivalent to `IsLocalization.mk'` when the latter is applied to the localization of `R` at `M`. In other words, both functions, which construct elements of the localization, are the same in this context. The `Localization.mk` function constructs an element of the localization by sending a pair `(x, y)` to its equivalence class under the localization relation, while `IsLocalization.mk'` does it by mapping `(x, y)` to the element `f(x) * (f(y))⁻¹` in the localization. Here, `f` is a function that maps elements of `R` to elements of the localization.
More concisely: For any commutative semiring `R` and submonoid `M`, the `Localization.mk` and `IsLocalization.mk'` functions constructing elements in the localization of `R` at `M` are equal.
|
IsLocalization.ext
theorem IsLocalization.ext :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] (j k : S → P),
j 1 = 1 →
k 1 = 1 →
(∀ (a b : S), j (a * b) = j a * j b) →
(∀ (a b : S), k (a * b) = k a * k b) →
(∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)) → j = k
This theorem, `IsLocalization.ext`, states that in order to show that two mappings `j` and `k` from a localized ring `S` to a commutative semiring `P` agree on the entirety of the localization, it is enough to demonstrate that they agree on the image of the base ring `R`. This is under the conditions that both `j` and `k` preserve the multiplicative identity `1` and the multiplication operation `*`. More specifically, if `j(1) = 1`, `k(1) = 1`, `j(a * b) = j(a) * j(b)` and `k(a * b) = k(a) * k(b)` for all `a` and `b` in `S`, and `j` and `k` agree on the image of any `a` in `R` under the algebra map from `R` to `S`, then `j = k`.
More concisely: Given homomorphisms j and k from a localized ring S to a commutative semiring P preserving the multiplicative identity and multiplication, if they agree on the image of the base ring under the algebra map and j(a\*b) = j(a) \* j(b) and k(a\*b) = k(a) \* k(b) for all a, b in S, then j = k.
|
IsField.localization_map_bijective
theorem IsField.localization_map_bijective :
∀ {R : Type u_4} {Rₘ : Type u_5} [inst : CommRing R] [inst_1 : CommRing Rₘ] {M : Submonoid R},
0 ∉ M →
IsField R → ∀ [inst_2 : Algebra R Rₘ] [inst_3 : IsLocalization M Rₘ], Function.Bijective ⇑(algebraMap R Rₘ)
The theorem `IsField.localization_map_bijective` states that for any types `R` and `Rₘ`, where `R` is a commutative ring, `Rₘ` is a commutative ring, and `M` is a submonoid of `R` that does not contain 0, if `R` is a field (a commutative ring where every non-zero element has a multiplicative inverse), and there is an algebraic structure and a localization structure relating `R` and `Rₘ`, then the algebraic mapping from `R` to `Rₘ` is a bijective function. In other words, if `R` is a field, then localizing at a submonoid not containing `0` does not add any new elements to the ring.
More concisely: If `R` is a field and `M` is a submonoid of `R` not containing 0, then the localization mapping from `R` to `R_M` is a bijective function. (Here, `R_M` denotes the localization of `R` at `M`.)
|
Localization.add_mk_self
theorem Localization.add_mk_self :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (a : R) (b : ↥M) (c : R),
Localization.mk a b + Localization.mk c b = Localization.mk (a + c) b
This theorem, `Localization.add_mk_self`, states that for any given commutative semiring `R`, a submonoid `M` of `R`, an element `a` of `R`, an element `b` of `M`, and an element `c` of `R`, the sum of the localized elements `Localization.mk a b` and `Localization.mk c b` is equal to the localized element `Localization.mk (a + c) b`. In other words, this theorem establishes the addition operation's behavior in the localization of a commutative semiring at a submonoid, showing that the addition of localized elements corresponds to the localization of their sum in the original semiring.
More concisely: For any commutative semiring R, submonoid M, and elements a, b, c in R, the localization of a + c at b in R equals the localization of a at b plus the localization of c at b.
|
IsLocalization.eq_mk'_iff_mul_eq
theorem IsLocalization.eq_mk'_iff_mul_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} {y : ↥M} {z : S},
z = IsLocalization.mk' S x y ↔ z * (algebraMap R S) ↑y = (algebraMap R S) x
This theorem, named `IsLocalization.eq_mk'_iff_mul_eq`, establishes an equivalence in the context of IsLocalization, a concept in algebraic geometry and commutative algebra. Given a commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S`, and an algebra structure from `R` to `S` that makes `S` a localization of `R` at `M`, the theorem states that for any element `x` of `R`, element `y` of `M`, and `z` of `S`, `z` equals the result of the function `IsLocalization.mk'` applied to `S`, `x`, and `y` if and only if the product of `z` and the image of `y` under the algebra mapping from `R` to `S` is equal to the image of `x` under the same algebra mapping. This theorem basically gives a condition for equating an element in the target semiring with a fraction-like expression in terms of the algebra map and elements from the original ring and submonoid.
More concisely: For an algebra structure from a commutative semiring `R` to a commutative semiring `S` making `S` a localization of `R` at a submonoid `M`, `IsLocalization.mk'(S, x, y) = z` if and only if `z * S.algebra_map R x = S.algebra_map R y * x`.
|
IsLocalization.ringHom_ext
theorem IsLocalization.ringHom_ext :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] ⦃j k : S →+* P⦄,
j.comp (algebraMap R S) = k.comp (algebraMap R S) → j = k
The theorem `IsLocalization.ringHom_ext` states that for any commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S` that is a localization of `R` at `M`, and any other commutative semiring `P`, if there are two ring homomorphisms `j` and `k` from `S` to `P` such that the composition of `j` or `k` with the algebra map from `R` to `S` are equal, then `j` and `k` have to be equal. In other words, this theorem asserts the uniqueness of a ring homomorphism when extended by a fixed algebra map.
More concisely: Given commutative semirings R, a submonoid M of R, a localization S of R at M, and commutative semirings P, if two ring homomorphisms j and k from S to P make their compositions with the algebra map from R to S equal, then j = k.
|
IsLocalization.mk'_eq_iff_eq_mul
theorem IsLocalization.mk'_eq_iff_eq_mul :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} {y : ↥M} {z : S},
IsLocalization.mk' S x y = z ↔ (algebraMap R S) x = z * (algebraMap R S) ↑y
The theorem `IsLocalization.mk'_eq_iff_eq_mul` establishes an equivalency relation in the context of ring theory and algebraic structures. Specifically, for any commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S`, a ring homomorphism between `R` and `S`, and elements `x` of `R`, `y` of `M` and `z` of `S`. The theorem states that the mapping of `(x, y)` in `R × M` to `f(x) * (f(y))⁻¹` in `S` (where `f` is the function defined by `IsLocalization.mk'`) is equivalent to `z` if and only if the image of `x` under the algebra map from `R` to `S` is equal to `z` multiplied by the image of `y` under the same algebra map. Here, `algebraMap R S` represents the ring homomorphism from `R` to `S` induced by the given algebra structure.
More concisely: For any commutative semiring `R`, submonoid `M` of `R`, commutative semiring `S`, ring homomorphism `f: R -> S`, and elements `x in R`, `y in M`, and `z in S`, `(x, y) in R × M` maps to `z` under `IsLocalization.mk'` if and only if `f(x) = z * f(y)`.
|
IsLocalization.mk'_one
theorem IsLocalization.mk'_one :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R), IsLocalization.mk' S x 1 = (algebraMap R S) x
The theorem `IsLocalization.mk'_one` states that for any commutative semiring `R`, submonoid `M` of `R`, and `S` being a localization of `R` at `M`, and any element `x` in `R`, the image of the pair `(x, 1)` under the surjective function `IsLocalization.mk' S` (which sends a pair `(x, y)` in `R × M` to `f x * (f y)⁻¹`) is equal to the image of `x` under the algebra map from `R` to `S`. In mathematical terms, this means that for any `x` in `R`, we have `f(x) * (f(1))⁻¹ = f(x)`, where `f` is the algebra map from `R` to `S`.
More concisely: For any commutative semiring `R`, submonoid `M` of `R`, localization `S` of `R` at `M`, and `x` in `R`, the image of `(x, 1)` under `IsLocalization.mk' S` equals the image of `x` under the algebra map from `R` to `S`. In other words, `f(x) * f(1)⁻¹ = f(x)`, where `f` is the algebra map.
|
IsLocalization.lift_eq
theorem IsLocalization.lift_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
(hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R), (IsLocalization.lift hg) ((algebraMap R S) x) = g x
The theorem `IsLocalization.lift_eq` states that for any commutative semirings `R`, `S`, and `P`, a submonoid `M` of `R`, and an algebra structure on `R` and `S`, if `S` is a localization of `R` at `M`, and `g` is a ring homomorphism from `R` to `P` such that each element of `M` is a unit under `g`, then for every element `x` of `R`, applying the localization lift `IsLocalization.lift` to the algebra map of `x` from `R` to `S` yields the same result as applying `g` directly to `x`. In other words, the diagram commutes. The localization lift is a way of extending a map defined on `R` to a map defined on the localization of `R` at `M`.
More concisely: If `R` is a commutative semiring, `M` a submonoid of `R`, `S` a localization of `R` at `M`, `g` a ring homomorphism from `R` to a ring `P` such that each element of `M` is a unit under `g`, then for all `x` in `R`, `IsLocalization.lift(algebraMap x) = g x`.
|
IsLocalization.isDomain_localization
theorem IsLocalization.isDomain_localization :
∀ {A : Type u_6} [inst : CommRing A] [inst_1 : IsDomain A] {M : Submonoid A},
M ≤ nonZeroDivisors A → IsDomain (Localization M)
This theorem states that the localization of an integral domain to a set of its non-zero elements is also an integral domain. Here, an integral domain is a kind of commutative ring in which the product of any two non-zero elements is always non-zero. Localization, in this context, is a process that adds multiplicative inverses to a mathematical structure. The theorem hence asserts that if we start with an integral domain (represented by `A`) and take its localization with respect to a submonoid `M` of non-zero elements (i.e., elements for which the product with any other element never results in zero), then the resulting structure remains an integral domain.
More concisely: The localization of an integral domain with respect to a submonoid of non-zero elements is still an integral domain.
|
IsLocalization.mk'_spec
theorem IsLocalization.mk'_spec :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
IsLocalization.mk' S x y * (algebraMap R S) ↑y = (algebraMap R S) x
The theorem `IsLocalization.mk'_spec` states that for any commutative semiring `R`, submonoid `M` of `R`, and a type `S` which is a commutative semiring, an `R`-algebra, and a localization of `R` at `M`, the operation `IsLocalization.mk' S x y` followed by multiplication by the image of `y` under the algebra mapping from `R` to `S`, equals the image of `x` under the same algebra mapping. In mathematical terms, it says that for any `x` in `R` and `y` in `M`, `f(x) * (f(y))^(-1) * f(y) = f(x)`, where `f` is the algebra map from `R` to `S`. Here, `f(x) * (f(y))^(-1)` is the surjection of the pair `(x, y)` by `IsLocalization.mk' S`.
More concisely: For any commutative semiring `R`, submonoid `M` of `R`, and an `R`-algebra `S` that is a localization of `R` at `M`, the algebra map `f: R -> S` satisfies `f(x) = f(x) * (f(y))^(-1) * f(y)` for all `x in R` and `y in M`.
|
IsLocalization.lift_mk'
theorem IsLocalization.lift_mk' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
(hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R) (y : ↥M),
(IsLocalization.lift hg) (IsLocalization.mk' S x y) = g x * ↑((IsUnit.liftRight (g.restrict M) hg) y)⁻¹
This theorem states that given a commutative semiring `R`, a submonoid `M` of `R`, and a localization map `f : R →+* S` for `M`, if we also have a homomorphism `g : R →* P` of commutative semirings such that for every element `y` in `M`, `g y` is a unit in `P`, then for every `x` in `R` and `y` in `M`, the homomorphism induced from `S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹`. In other words, the homomorphism preserves the structure of the localization.
More concisely: Given a commutative semiring `R`, a submonoid `M` of `R`, a localization map `f : R →+* S` for `M`, and a homomorphism `g : R →* P` of commutative semirings such that `g(y)` is a unit in `P` for every `y` in `M`, the homomorphism `h : S → P` induced from `f` satisfies `h(f(x) * f(y)⁻¹) = g(x) * g(y)⁻¹` for all `x` in `R` and `y` in `M`.
|
IsLocalization.monoidHom_ext
theorem IsLocalization.monoidHom_ext :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] ⦃j k : S →* P⦄,
j.comp ↑(algebraMap R S) = k.comp ↑(algebraMap R S) → j = k
This theorem, `IsLocalization.monoidHom_ext`, states that for any commutative semiring `R`, any submonoid `M` of `R`, any commutative semiring `S` for which there exists an algebra structure over `R`, and any type `P` with a commutative semiring structure, if `S` is a localization of the submonoid `M`, then for any two monoid homomorphisms `j` and `k` from `S` to `P`, if the composition of `j` and the algebra map from `R` to `S` equals the composition of `k` and the algebra map from `R` to `S`, then `j` equals `k`.
In simpler terms, it says that if two monoid homomorphisms from a localization of a commutative semiring to another commutative semiring coincide when composed with the algebra map from the original semiring, then these two homomorphisms are actually the same.
More concisely: If `M` is a submonoid of a commutative semiring `R`, `S` is a localization of `M`, and `j` and `k` are monoid homomorphisms from `S` to a commutative semiring `P` such that `j ∘ a = k ∘ a`, where `a` is the algebra map from `R` to `S`, then `j = k`.
|
IsLocalization.map_units'
theorem IsLocalization.map_units' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [self : IsLocalization M S] (y : ↥M), IsUnit ((algebraMap R S) ↑y)
This theorem states that for any commutative semiring `R`, any submonoid `M` of `R`, and any commutative semiring `S` with an algebra structure over `R` that is a localization of `M`, every element `y` in the submonoid `M` maps to a unit in `S` under the algebra map from `R` to `S`. In other words, any element of `M` becomes invertible in `S` when mapped via the algebra structure.
More concisely: For any commutative semirings `R`, submonoid `M` of `R`, and commutative semiring `S` with an `R`-algebra structure that is a localization of `M`, every element in `M` maps to a unit in `S` under the algebra map.
|
IsLocalization.map_map
theorem IsLocalization.map_map :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
{T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] (hy : M ≤ Submonoid.comap g T) [inst_6 : Algebra P Q]
[inst_7 : IsLocalization T Q] {A : Type u_5} [inst_8 : CommSemiring A] {U : Submonoid A} {W : Type u_6}
[inst_9 : CommSemiring W] [inst_10 : Algebra A W] [inst_11 : IsLocalization U W] {l : P →+* A}
(hl : T ≤ Submonoid.comap l U) (x : S),
(IsLocalization.map W l hl) ((IsLocalization.map Q g hy) x) = (IsLocalization.map W (l.comp g) ⋯) x
The theorem `IsLocalization.map_map` states that given the homomorphisms `g : R →+* P` and `l : P →+* A` between commutative semirings, if these homomorphisms induce maps of localizations, then the composition of the induced maps is equal to the map of localizations induced by the composition `l ∘ g`. More explicitly, for any element `x` in the localization `S` of `R` at `M`, the map from `S` to `W` induced by `l`, applied to the map from `S` to `Q` induced by `g`, applied to `x`, equals the map from `S` to `W` induced by `l ∘ g`, applied to `x`. This holds under the hypotheses that `M` is contained in the preimage of `T` under `g` and `T` is contained in the preimage of `U` under `l`.
More concisely: Given commutative semirings R, P, and A, homomorphisms g : R ->* P and l : P ->* A with induced localization maps, if M is in the preimage of T under g and T is in the preimage of U under l, then the induced map from S (the localization of R at M) to W (the localization of A at U) obtained from composing g and l is equal to the map obtained by first applying l to the map induced by g from S to Q (the localization of P at T).
|
Localization.add_mk
theorem Localization.add_mk :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (a : R) (b : ↥M) (c : R) (d : ↥M),
Localization.mk a b + Localization.mk c d = Localization.mk (↑b * c + ↑d * a) (b * d)
The `Localization.add_mk` theorem states that for any commutative semiring `R` and any submonoid `M` of `R`, given elements `a` and `c` of `R`, and `b` and `d` from `M`, the sum of the localizations of `a` at `b` and `c` at `d` is the localization of `bc + da` at the product `bd`. In other words, the theorem articulates how addition works in the localization of a commutative ring at a submonoid.
More concisely: For any commutative semiring R and submonoid M, the localization of (bc + da) at bd is the sum of the localizations of a at b and c at d in R.
|
Localization.neg_mk
theorem Localization.neg_mk :
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (a : R) (b : ↥M),
-Localization.mk a b = Localization.mk (-a) b
This theorem states that for any commutative ring `R` and any submonoid `M` of `R`, for any element `a` of `R` and any element `b` of `M`, the negation of the localization of `R` at `M` of the pair `(a, b)` is equal to the localization of `R` at `M` of the pair `(-a, b)`. In other words, negating the equivalence class of `(a, b)` in the localization of `R` at `M` results in the equivalence class of `(-a, b)`. This is a property of localization in the context of commutative ring theory.
More concisely: For any commutative ring `R` and submonoid `M`, the negative of the localization of `(a, b)` in `R` at `M` equals the localization of `(-a, b)` in `R` at `M`, for all `a` in `R` and `b` in `M`.
|
IsLocalization.surj
theorem IsLocalization.surj :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
The theorem `IsLocalization.surj` states that for any commutative semiring `R`, any submonoid `M` of `R`, any commutative semiring `S`, and any algebra structure from `R` to `S`, if `S` is a localization of `R` at `M`, then for every element `z` in `S`, there exists an element `x` such that `z` multiplied by the image of the second component of `x` under the algebra map from `R` to `S` equals the image of the first component of `x` under the same algebra map. In other words, every element `z` of `S` is in the image of the multiplication by some element of `M` of the algebra map from `R` to `S`.
More concisely: If `S` is a localization of commutative semiring `R` at submonoid `M` via an algebra structure from `R` to `S`, then for every `z` in `S`, there exists `x` in `R` such that `z = x * m * s`, where `m` is in `M` and `s` is the image of `x` under the algebra map from `R` to `S`.
|
IsLocalization.lift_comp
theorem IsLocalization.lift_comp :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
(hg : ∀ (y : ↥M), IsUnit (g ↑y)), (IsLocalization.lift hg).comp (algebraMap R S) = g
The theorem `IsLocalization.lift_comp` states that, given a commutative semiring `R`, a submonoid `M` of `R`, another commutative semiring `S` with an algebra structure over `R`, and yet another commutative semiring `P`, along with an indication that `S` is a localization of `R` at `M`, and a ring homomorphism `g` from `R` to `P` that maps each element of `M` to a unit in `P`, then the composition of the ring homomorphism `IsLocalization.lift hg` (constructed from `g` and `hg`) and the ring homomorphism generated by the algebra structure of `S` over `R` (`algebraMap R S`) is the same as the original ring homomorphism `g`. In simpler terms, this theorem expresses a fundamental property of the localization process in commutative algebra, ensuring the existence of a certain homomorphisms compatibility when working with localizations.
More concisely: Given a commutative semiring `R`, a submonoid `M` of `R`, a localization of `R` at `M` `S`, a ring homomorphism `g : R → P` mapping `M` to units in `P`, the homomorphism `IsLocalization.lift hg` constructed from `g` and `hg` equals the composition of `g` with the algebra homomorphism `algebraMap R S`.
|
IsLocalization.mk'_self
theorem IsLocalization.mk'_self :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} (hx : x ∈ M), IsLocalization.mk' S x ⟨x, hx⟩ = 1
The theorem `IsLocalization.mk'_self` states that for any commutative semiring `R` and any submonoid `M` of `R`, if `S` is a localization of `R` at `M`, then for any element `x` in `M`, the value of `IsLocalization.mk' S x` applied to `x` is `1`. In other words, it states that when the function `IsLocalization.mk'` is applied to `a` of `M` and `{ val := a, property := hx }` (which is just `a` again packaged with a proof that it is in `M`), the result is always `1`. This is an important property in the theory of localization of rings.
More concisely: For any commutative semiring `R`, submonoid `M` of `R`, and localization `S` of `R` at `M`, the application of `IsLocalization.mk' S` to any element `x` in `M` results in `1`.
|
IsLocalization.isDomain_of_le_nonZeroDivisors
theorem IsLocalization.isDomain_of_le_nonZeroDivisors :
∀ {S : Type u_2} [inst : CommRing S] (A : Type u_6) [inst_1 : CommRing A] [inst_2 : IsDomain A]
[inst_3 : Algebra A S] {M : Submonoid A} [inst_4 : IsLocalization M S], M ≤ nonZeroDivisors A → IsDomain S
The theorem `IsLocalization.isDomain_of_le_nonZeroDivisors` states that for any commutative ring `S` that is a localization of an integral domain `R` at a subset of non-zero elements, `S` is also an integral domain. This is under the condition that the monoid `M` of localization elements from `R` is a subset of the non-zero divisors of `R`. Non-zero divisors are elements that when multiplied by any element of the ring result in a non-zero product. The theorem essentially implies that localizing an integral domain at a subset of non-zero elements preserves the property of being an integral domain.
More concisely: If `R` is an integral domain and `S` is its localization at a subset of non-zero divisors, then `S` is also an integral domain.
|
IsLocalization.eq_of_eq
theorem IsLocalization.eq_of_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P},
(∀ (y : ↥M), IsUnit (g ↑y)) → ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → g x = g y
Given a localization map `f` from a commutative semiring `R` to another commutative semiring `S` for a submonoid `M` of `R`, and a map `g` from `R` to a commutative semiring `P` such that the image of `M` under `g` lies within the units of `P`, the theorem states that if the images of `x` and `y` (elements of `R`) under the algebra map from `R` to `S` are equal, then the images of `x` and `y` under `g` are also equal. In other words, if `f(x) = f(y)`, then `g(x) = g(y)`, for all `x` and `y` in the commutative semiring `R`.
More concisely: If `f : R -> S` is a localization map of a commutative semiring `R` to another commutative semiring `S` for a submonoid `M` of `R`, and `g : R -> P` maps `M` into the units of a commutative semiring `P`, then `x ∈ R` implies `f(x) = f(y)` if and only if `g(x) = g(y)`.
|
IsLocalization.map_eq
theorem IsLocalization.map_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
{T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] (hy : M ≤ Submonoid.comap g T) [inst_6 : Algebra P Q]
[inst_7 : IsLocalization T Q] (x : R),
(IsLocalization.map Q g hy) ((algebraMap R S) x) = (algebraMap P Q) (g x)
The theorem `IsLocalization.map_eq` states that for any commutative semiring `R`, a submonoid `M` of `R`, a commutative semiring `S` such that `S` is a localization of `R` at `M`, a monoid homomorphism `g` from `R` to a commutative semiring `P`, a submonoid `T` of `P`, and a commutative semiring `Q` such that `Q` is a localization of `P` at `T`, if `M` is a subset of the preimage of `T` under `g`, then for any element `x` of `R`, the result of first applying the algebra map from `R` to `S` to `x`, then applying the map from `S` to `Q` induced by `g`, is the same as the result of first applying `g` to `x`, then applying the algebra map from `P` to `Q`.
In mathematical terms, this theorem states that the following diagram commutes:
```
R --(algebraMap R S)--> S --(IsLocalization.map Q g hy)--> Q
| |
| |
V V
P --(algebraMap P Q)--> Q
```
where the vertical arrows are the map `g` and the horizontal arrows are the algebra maps.
More concisely: For commutative semirings R, S (a localization of R at a submonoid M), P, and Q (a localization of P at a submonoid T), and a monoid homomorphism g from R to P with M a subset of g^-1(T), the diagram commutes, i.e., algebraMap R S (x) = IsLocalization.map Q g (algebraMap P Q (g x)) for all x in R.
|
IsLocalization.surj'
theorem IsLocalization.surj' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [self : IsLocalization M S] (z : S),
∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
This theorem states that for any commutative semiring `R`, any submonoid `M` of `R`, and any commutative semiring `S` with an algebra structure over `R`, if `S` is a localization of `R` at `M`, then for every element `z` in `S`, there exists an element `x` in `R` such that the multiplication of `z` and the image of the second component of `x` under `algebraMap` is equal to the image of the first component of `x` under `algebraMap`. In mathematical terms, for every `z` in `S`, there exists `x` in `R` such that $z \cdot \text{algebraMap}(x_2) = \text{algebraMap}(x_1)$, suggesting that the `algebraMap` is surjective.
More concisely: For any commutative semirings `R`, submonoid `M` of `R`, and commutative semiring `S` with an algebra structure over `R` being a localization of `R` at `M`, the algebra map from `R` to `S` is surjective.
|
IsLocalization.eq_iff_exists
theorem IsLocalization.eq_iff_exists :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x y : R},
(algebraMap R S) x = (algebraMap R S) y ↔ ∃ c, ↑c * x = ↑c * y
The theorem `IsLocalization.eq_iff_exists` states that for any commutative semiring `R`, submonoid `M` of `R`, another commutative semiring `S`, and an algebra structure from `R` to `S`, if `S` is a localization of `R` at `M`, then for any two elements `x` and `y` of `R`, the image of `x` under the algebra map to `S` is equal to the image of `y` under the same map if and only if there exists an element `c` in `M` such that `c` times `x` equals `c` times `y`.
This theorem asserts that two elements map to the same value under the algebra map if they can be made equivalent by multiplication with an element from the localizing submonoid.
More concisely: For any commutative semirings R, S, a commutative algebra structure from R to S, and a submonoid M of R such that S is a localization of R at M, x and y in R map to the same image under the algebra map if and only if there exists m in M such that x = my/m.
|
IsLocalization.map_injective_of_injective
theorem IsLocalization.map_injective_of_injective :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
(Q : Type u_4) [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q],
Function.Injective ⇑g →
∀ [inst_7 : IsLocalization (Submonoid.map g M) Q], Function.Injective ⇑(IsLocalization.map Q g ⋯)
This theorem states that the injectivity of a function carries over to the function induced on localizations. Specifically, given a function `g` from a type `R` to a type `P` where `R` and `P` are both commutative semirings, if `g` is injective, then the function induced on localizations is also injective. Here, the localization is created with respect to a submonoid `M` of `R` and a submonoid obtained by mapping `M` through `g`.
More concisely: If `g` is a function from a commutative semiring `R` to another commutative semiring `P` such that `g` is injective, then the induced function on localizations of `R` and `P` with respect to submonoids `M` and its image under `g`, respectively, is also injective.
|
IsLocalization.mk'_spec'
theorem IsLocalization.mk'_spec' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
(algebraMap R S) ↑y * IsLocalization.mk' S x y = (algebraMap R S) x
The theorem `IsLocalization.mk'_spec'` states that for any commutative semiring `R`, a submonoid `M` of `R`, a type `S` which is also a commutative semiring, an algebra structure on `R` and `S`, and an instance proving that `S` is a localization of `R` at `M`, for any elements `x` of `R` and `y` of `M`, the result of mapping `y` into `S` using the algebra structure and then multiplying by the result of localizing `x` at `y` is equal to the result of mapping `x` into `S` using the algebra structure. In mathematical terms, it says that if S is a localization of R at M, then for all x in R and y in M, we have that $ϕ(y) * (ϕ(x) / ϕ(y)) = ϕ(x)$, where $ϕ$ is the algebra map from R to S.
More concisely: For any commutative semirings R and S, submonoid M of R, algebra structures on R and S, and instance of S being a localization of R at M, for all x in R and y in M, we have $ϕ(y) * (ϕ(x) / ϕ(y)) = ϕ(x)$ where $ϕ$ is the algebra map from R to S.
|
IsLocalization.algebraMap_eq_map_map_submonoid
theorem IsLocalization.algebraMap_eq_map_map_submonoid :
∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
(Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
[inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ] [inst_10 : IsScalarTower R Rₘ Sₘ]
[inst_11 : IsScalarTower R S Sₘ], algebraMap Rₘ Sₘ = IsLocalization.map Sₘ (algebraMap R S) ⋯
This theorem states that for any commutative rings R, S, Rₘ, Sₘ, a submonoid M of R, and given algebra structures between these rings, if Rₘ and Sₘ are localizations of R and S at M and M mapped to S respectively, and if the algebra structures form a scalar tower (meaning that scalar multiplication is compatible in a certain sense), then the algebra map from Rₘ to Sₘ is uniquely determined by the map from Sₘ that comes from localizing the algebra map from R to S. This is formalizing that a certain commutative diagram (a diagram where all paths give the same result) actually commutes.
More concisely: Given commutative rings R, S, their algebras R��မ, S⁛, a submonoid M of R, and localizations R⁘, S⁘ of R and S at M with compatible scalar towers, the unique algebra map from R⁘ to S⁘ is determined by the localized algebra map from R to S.
|
Field.localization_map_bijective
theorem Field.localization_map_bijective :
∀ {K : Type u_4} {Kₘ : Type u_5} [inst : Field K] [inst_1 : CommRing Kₘ] {M : Submonoid K},
0 ∉ M → ∀ [inst_2 : Algebra K Kₘ] [inst_3 : IsLocalization M Kₘ], Function.Bijective ⇑(algebraMap K Kₘ)
The theorem `Field.localization_map_bijective` states that for any field `K` and any commutative ring `Kₘ`, given a submonoid `M` of `K` that does not contain the element `0`, and given that `Kₘ` is a localization of `K` at `M`, the function that maps `K` to `Kₘ` (given by the algebra structure) is bijective. In simpler terms, when we localize a field at a submonoid that does not contain `0`, we do not add any new elements to the field.
More concisely: The localization map from a field `K` to its localization at a submonoid `M` that does not contain `0` is a bijective ring homomorphism.
|