IsLocalization.Away.lift.proof_1
theorem IsLocalization.Away.lift.proof_1 :
∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_2} [inst_1 : CommSemiring P] (x : R) {g : R →+* P},
IsUnit (g x) → ∀ (y : ↥(Submonoid.powers x)), IsUnit (g ↑y)
This theorem, `IsLocalization.Away.lift.proof_1`, states that for any commutative semiring `R`, any type `P` that is also a commutative semiring, any element `x` of `R`, and any ring homomorphism `g` from `R` to `P`, if `x` is a unit under the ring homomorphism `g`, then for any element `y` in the submonoid generated by `x`, `y` will also be a unit under the ring homomorphism `g`. In simpler terms, if `x` has a two-sided inverse under a certain mapping, then any power of `x` also has a two-sided inverse under the same mapping.
More concisely: If `x` is a unit in `R` under the ring homomorphism `g`, then for every `y` in the submonoid generated by `x`, `y` is also a unit in `P` under `g`.
|
selfZPow_of_nonneg
theorem selfZPow_of_nonneg :
∀ {R : Type u_1} [inst : CommRing R] (x : R) (B : Type u_2) [inst_1 : CommRing B] [inst_2 : Algebra R B]
[inst_3 : IsLocalization.Away x B] {n : ℤ}, 0 ≤ n → selfZPow x B n = (algebraMap R B) x ^ n.natAbs
The theorem `selfZPow_of_nonneg` states that, given a commutative ring `R`, an element `x` in `R`, a commutative ring `B`, and an algebra structure from `R` to `B`, if `B` is isomorphic to the localization of `R` at the submonoid generated by `x`, then for any integer `n` that is nonnegative, the result of applying the `selfZPow` function to `x` and `n` is equivalent to mapping `x` into `B` using the algebra structure and then raising it to the power of the absolute value of `n`. In simpler terms, it relates the power operations in the original ring and the localized ring when the exponent is a nonnegative integer.
More concisely: If `R` is a commutative ring, `x` is an element of `R`, `B` is isomorphic to the localization of `R` at the submonoid generated by `x`, and `n` is a nonnegative integer, then `x ^ n` in `B` is equivalent to applying the algebra homomorphism from `R` to `B` to `x` and then raising the result to the power of `n`.
|
IsLocalization.Away.mul_invSelf
theorem IsLocalization.Away.mul_invSelf :
∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
[inst_3 : IsLocalization.Away x S], (algebraMap R S) x * IsLocalization.Away.invSelf x = 1
The theorem `IsLocalization.Away.mul_invSelf` states that for any commutative semiring `R`, any commutative semiring `S` and any algebra structure from `R` to `S`, and for any element `x` of `R` such that `S` is a localization of `R` at the submonoid generated by `x`, the product of the image of `x` under the algebra's structure map and the inverse of `x` in the localization equals 1. In other words, this theorem establishes that the image of `x` under the algebra's structure map is a unit in the localization, and its inverse is `IsLocalization.Away.invSelf x`. This is analogous to the usual property in field theory that asserts the product of a non-zero element and its multiplicative inverse equals 1.
More concisely: Given a commutative semiring `R`, a commutative semiring `S`, an algebra structure from `R` to `S`, and an element `x` in `R` such that `S` is a localization of `R` at the submonoid generated by `x`, then the image of `x` under the algebra's structure map and the inverse of `x` in the localization multiply to 1.
|
IsLocalization.Away.AwayMap.lift_eq
theorem IsLocalization.Away.AwayMap.lift_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
{P : Type u_3} [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {g : R →+* P}
(hg : IsUnit (g x)) (a : R), (IsLocalization.Away.lift x hg) ((algebraMap R S) a) = g a
This theorem, named `IsLocalization.Away.AwayMap.lift_eq`, states that for all types `R`, `S`, and `P` which are structures of commutative semirings with `R` and `S` being algebras, there exists an element `x` in `R` such that `S` is isomorphic to the localization of `R` at the submonoid generated by `x`. Given a ring homomorphism `g` from `R` to `P` such that `g(x)` is a unit (i.e., it has a two-sided inverse), and an element `a` in `R`, applying the lift of the localization of `R` at `x`, followed by the embedding of `R` into `S`, to `a` is equivalent to applying `g` to `a`. In other words, the diagram commutes. This theorem is fundamental in the study of localizations in algebra, linking properties of original rings to their localizations.
More concisely: Given commutative semirings R, S, and P with R and S being algebras, an element x in R, a ring homomorphism g from R to P with g(x) a unit, and an element a in R, the diagram commutes: localization of R at x in S ≅ {b in S | ∃ c in R, g(c) = b and cx = xa} → a → g(a).
|