IsLocalization.exist_integer_multiples_of_finite
theorem IsLocalization.exist_integer_multiples_of_finite :
∀ {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] {ι : Type u_4} [inst_4 : Finite ι] (f : ι → S),
∃ b, ∀ (i : ι), IsLocalization.IsInteger R (↑b • f i)
This theorem states that given a commutative semiring `R`, a submonoid `M` of `R`, and an algebra `S` that is a localization of `R` at `M`, for any finite indexed family of elements of `S` (denoted by the function `f` from index set `ι` to `S`), there exists an element `b` in the submonoid `M` such that for all indices `i` in `ι`, the scaled value `b * f(i)` is an integer within the algebra from `R` to `S`. In other words, we can clear the denominators of a finite indexed family of fractions in the localization.
More concisely: Given a commutative semiring `R`, a submonoid `M` of `R`, and an algebra `S` that is a localization of `R` at `M`, for any finite indexed family `f` of elements from `S`, there exists an element `b` in `M` such that `b * f(i)` is an integer in `R` for all indices `i`.
|
IsLocalization.exists_integer_multiple
theorem IsLocalization.exists_integer_multiple :
∀ {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] (a : S), ∃ b, IsLocalization.IsInteger R (↑b • a)
This theorem states that for any given element `a` of a type `S` (which is a localization of type `R`), there exists an element `b` from the submonoid `M` of `R` such that the scalar multiplication of `b` and `a` is an integer in the localization. Specifically, this version of the theorem multiplies `a` on the left, matching the argument order in the `SMul` instance.
In mathematical terms, given a commutative semiring `R`, a submonoid `M` of `R`, and a commutative semiring `S` which is a localization of `R` at `M`, for every element `a` in `S`, there exists an element `b` in `M` such that the product `b*a` is in the image of the localization map from `R` to `S`.
More concisely: For every element `a` in a localization `S` of a commutative semiring `R` at a submonoid `M`, there exists an element `b` in `M` such that `b*a` is in the image of the localization map from `R` to `S`.
|
IsLocalization.exist_integer_multiples
theorem IsLocalization.exist_integer_multiples :
∀ {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] {ι : Type u_4} (s : Finset ι) (f : ι → S),
∃ b, ∀ i ∈ s, IsLocalization.IsInteger R (↑b • f i)
This theorem states that given a commutative semiring `R`, a submonoid `M` of `R`, and another commutative semiring `S` that is a localization of `R` at `M`, for any index set `ι` and any finite set `s` of indices from `ι`, there is a function `f` from `ι` to `S`. The theorem then asserts the existence of an element `b` such that for every index `i` in the finite set `s`, the scalar multiple `b • f(i)` is an integer of `R` - which means that it lies in the image of the localization map from `R` to `S`. In other words, we can find a common multiple `b` such that all elements of the `Finset`-indexed family of fractions `f(i)` are integers when scaled by `b`.
More concisely: Given a commutative semiring `R`, a submonoid `M` of `R`, and a localization `S` of `R` at `M`, for any index set `ι` and finite `ι`-indexed family `(f(i))_i` of elements in `S`, there exists an integer `b` in `R` such that `b • f(i)` is an element of `R` for all `i` in `ι`.
|
IsLocalization.exists_integer_multiple'
theorem IsLocalization.exists_integer_multiple' :
∀ {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] (a : S),
∃ b, IsLocalization.IsInteger R (a * (algebraMap R S) ↑b)
The theorem `IsLocalization.exists_integer_multiple'` states that for any given element `a` of a type `S` (which is a localization of `R`), there exists an element `b` in the submonoid `M` of `R` such that the product of `a` and the image of `b` under the algebra map from `R` to `S` is an integer. Here, "integer" refers to an element in the image of the algebra map from `R` to `S`. This theorem demonstrates a key property of localizations in commutative algebra, namely the existence of "integer multiples" within the localized set.
More concisely: For any element `a` in a localization `S` of a ring `R`, there exists an element `b` in the submonoid `M` of `R` such that `a * (image of b under the algebra map from R to S)` is an integer in `S`.
|
IsLocalization.exist_integer_multiples_of_finset
theorem IsLocalization.exist_integer_multiples_of_finset :
∀ {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] (s : Finset S),
∃ b, ∀ a ∈ s, IsLocalization.IsInteger R (↑b • a)
This theorem states that for any finite set of fractions in the localization `S` of a commutative semiring `R` with respect to a submonoid `M`, there exists an integer `b` in `R` such that when each fraction in the set is multiplied by `b`, the result is an integer in `R`. In other words, we can clear the denominators of a finite set of fractions in the localization.
More concisely: Given a finite set of fractions in the localization of a commutative semiring with respect to a submonoid, there exists an integer in the semiring that makes all the fractions in the set have integer values when multiplied by it.
|