IsFractionRing.lift_mk'
theorem IsFractionRing.lift_mk' :
∀ {A : Type u_4} [inst : CommRing A] [inst_1 : IsDomain A] {K : Type u_5} [inst_2 : Field K] {L : Type u_7}
[inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g)
(x : A) (y : ↥(nonZeroDivisors A)), (IsFractionRing.lift hg) (IsLocalization.mk' K x y) = g x / g ↑y
This theorem states that given an integral domain `A` with its field of fractions `K`, and an injective ring homomorphism `g` from `A` to a field `L`, there exists a field homomorphism that is induced from `K` to `L`. This induced homomorphism maps the fraction `f x / f y` (where `f` is a function from `A` to `K`) to the fraction `g x / g y` for all `x` in `A` and `y` in the set of non-zero divisors of `A`. The non-zero divisors of `A` are elements that do not zero out any other element when multiplied. The injectivity of `g` ensures that different elements in `A` are mapped to different elements in `L`.
More concisely: Given an integral domain `A` with its field of fractions `K`, an injective ring homomorphism `g` from `A` to a field `L`, there exists a unique field homomorphism extending `g` from `K` to `L`. The extended homomorphism maps `f x / f y` in `K` to `g x / g y` for all non-zero `f` in `A` and non-zero divisors `y` in `A`.
|
IsFractionRing.lift_algebraMap
theorem IsFractionRing.lift_algebraMap :
∀ {A : Type u_4} [inst : CommRing A] [inst_1 : IsDomain A] {K : Type u_5} [inst_2 : Field K] {L : Type u_7}
[inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g)
(x : A), (IsFractionRing.lift hg) ((algebraMap A K) x) = g x
This theorem states that given an integral domain `A` with its field of fractions `K`, and an injective ring homomorphism `g` from `A` to a field `L`, the field homomorphism induced from `K` to `L` maps any element `x` from `A` to `g(x)`. In other words, if we have a ring homomorphism from an integral domain to a field, and we extend this to a homomorphism from the field of fractions of the integral domain to the field, then this extended homomorphism acts the same way on elements of the integral domain as the original homomorphism.
More concisely: Given an integral domain `A` with field of fractions `K`, an integral domain homomorphism `g` from `A` to a field `L`, and the induced field homomorphism from `K` to `L`, we have `g(x) = (the induced homomorphism)(x)` for all `x` in `A`.
|
IsFractionRing.injective
theorem IsFractionRing.injective :
∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K], Function.Injective ⇑(algebraMap R K)
The theorem `IsFractionRing.injective` states that for any integral domain `R` with a commutative ring structure, and any field of fractions `K` of `R` which also has a commutative ring structure and an algebra structure over `R`, the algebra map that embeds `R` into `K` is injective. In other words, if `R` is mapped to `K` via the algebra map and two elements in `R` have the same image, then those two elements must be the same. This means that no information is lost when `R` is embedded into its field of fractions `K` using the algebra map.
More concisely: The algebra map embedding an integral domain `R` into its field of fractions `K` as an algebra over `R` is a injective ring homomorphism.
|
IsFractionRing.isDomain
theorem IsFractionRing.isDomain :
∀ (A : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A] {K : Type u_5} [inst_2 : CommRing K]
[inst_3 : Algebra A K] [inst : IsFractionRing A K], IsDomain K
The theorem `IsFractionRing.isDomain` states that for any commutative ring `A` that is an integral domain, and for any commutative ring `K` such that `K` is the field of fractions of `A`, `K` is also an integral domain. In simpler terms, it means that if you create a field of fractions (or field of quotients) from an integral domain, the result will also be an integral domain. This is a fundamental property in ring theory of mathematics.
More concisely: If `A` is a commutative integral domain, then the field of fractions `K` of `A` is also an integral domain.
|
IsFractionRing.to_map_eq_zero_iff
theorem IsFractionRing.to_map_eq_zero_iff :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] {x : R}, (algebraMap R K) x = 0 ↔ x = 0
This theorem, `IsFractionRing.to_map_eq_zero_iff`, states that for any commutative ring `R`, any commutative ring `K` which is the field of fractions of `R` (as specified by the `IsFractionRing R K` condition), and any `x` in `R`, the result of applying the algebra map (that is, the function that embeds `R` into `K` as specified by the algebra structure) to `x` is zero if and only if `x` is zero. In other words, the algebra map sends zero in `R` to zero in `K` and is injective at other values; it doesn't map any non-zero element of `R` to zero in `K`.
More concisely: For any commutative rings `R` and `K` with `IsFractionRing R K`, the algebra map from `R` to `K` sends `x` in `R` to zero in `K` if and only if `x` is zero in `R`.
|
IsFractionRing.mk'_eq_div
theorem IsFractionRing.mk'_eq_div :
∀ {A : Type u_4} [inst : CommRing A] [inst_1 : IsDomain A] {K : Type u_5} [inst_2 : Field K] [inst_3 : Algebra A K]
[inst_4 : IsFractionRing A K] {r : A} (s : ↥(nonZeroDivisors A)),
IsLocalization.mk' K r s = (algebraMap A K) r / (algebraMap A K) ↑s
The theorem `IsFractionRing.mk'_eq_div` states that for any commutative ring `A` that is an integral domain, and a field `K` such that `K` is the field of fractions of `A`, for any element `r` in `A` and `s` in the non-zero divisors of `A`, the map from `A × (non-zero divisors of A)` to `K` that sends `(r, s)` to `r/s` is equal to the result of applying the ring homomorphism from `A` to `K` to `r` and `s`, and then taking their division in `K`. This theorem essentially states that in the field of fractions of a ring, the fraction `r/s` is equal to the division of the images of `r` and `s` under the canonical map from the ring to its field of fractions.
More concisely: For any commutative integral domain ring A with field of fractions K, the map sending (r, s) to r/s from A × (non-zero divisors of A) equals the division of the ring homomorphism from A to K applied to r and s, i.e., r/s = (ρ(r) ÷ ρ(s)) in K, where ρ is the canonical homomorphism from A to K.
|