OreLocalization.oreDiv_mul_char
theorem OreLocalization.oreDiv_mul_char :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r₁ r₂ : R) (s₁ s₂ : ↥S)
(r' : R) (s' : ↥S), r₂ * ↑s' = ↑s₁ * r' → r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r' /ₒ (s₂ * s')
The theorem `OreLocalization.oreDiv_mul_char` states that for any type `R` that has a Monoid structure, a submonoid `S`, and an Ore set `S`, for any `r₁`, `r₂`, and `r'` in `R`, and `s₁`, `s₂`, and `s'` in `S`, if `r₂` times the canonical embedding of `s'` is equal to the canonical embedding of `s₁` times `r'`, then the Ore division of `r₁` by `s₁` times the Ore division of `r₂` by `s₂` equals the Ore division of `r₁` times `r'` by the multiplication of `s₂` and `s'`.
This theorem is a characterization of the multiplication operation in the Ore localization of a monoid, allowing for a choice of Ore numerator and Ore denominator.
More concisely: For any Monoid `R` with an Ore set `S`, if `r₂` times the embedding of `s'` equals the embedding of `s₁` times `r'`, then the Ore divisions of `r₁` by `s₁` and `r₂` by `s₂` are equal to the Ore division of `r₁` by `r'` times the product of `s₁` and `s₂`.
|
OreLocalization.ind
theorem OreLocalization.ind :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S]
{β : OreLocalization R S → Prop}, (∀ (r : R) (s : ↥S), β (r /ₒ s)) → ∀ (q : OreLocalization R S), β q
This theorem, `OreLocalization.ind`, is a principle of induction for the Ore localization of a monoid and a submonoid fulfilling the Ore condition. It states that for any type `R` equipped with a `Monoid` structure, and any submonoid `S` of `R` that fulfills the Ore condition, if a property `β` holds for all elements of the form `r /ₒ s` (where `r` is an element of `R` and `s` is an element of `S`), then this property `β` holds for all elements of the Ore localization of `R` and `S`. Essentially, it allows us to make deductions about all elements of the Ore localization based on the behavior of a subset of elements.
More concisely: If a property holds for all elements of the form r / s (r ∈ R, s ∈ S, where S is an Ore submonoid of the monoid R), then it holds for all elements in the Ore localization of R and S.
|
OreLocalization.oreDiv_eq_iff
theorem OreLocalization.oreDiv_eq_iff :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S},
r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ u v, r₂ * ↑u = r₁ * v ∧ ↑s₂ * ↑u = ↑s₁ * v
This theorem states that for any given type `R` with a Monoid structure, a submonoid `S` of `R`, an Ore set `inst_1` on `S`, and elements `r₁`, `r₂` of `R` and `s₁`, `s₂` of `S`, the division `r₁ /ₒ s₁` is equal to `r₂ /ₒ s₂` if and only if there exist elements `u` and `v` such that `r₂` times `u` equals `r₁` times `v` and `s₂` times `u` equals `s₁` times `v`. In other words, two fractions are equal in Ore's localization if and only if there is a cross-multiplication property between them.
More concisely: For any Monoid `R`, submonoid `S`, Ore set `inst_1`, and elements `r₁`, `r₂`, `s₁`, `s₂` in `R` with `S`, the fractions `r₁ /ₒ s₁` and `r₂ /ₒ s₂` are equal in Ore localization if and only if there exist `u` and `v` such that `r₁ * u = r₂ * v` and `s₁ * u = s₂ * v`.
|
OreLocalization.expand
theorem OreLocalization.expand :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S) (t : R)
(hst : ↑s * t ∈ S), r /ₒ s = r * t /ₒ ⟨↑s * t, hst⟩
This theorem states that for any given type `R` that is a Monoid, a submonoid `S` of `R`, a localization of `R` at `S`, and any elements `r` and `s` of `R` and `S` respectively, and an arbitrary element `t` of `R`, if the product of `s` and `t` is an element of `S` (denoted by `hst : ↑s * t ∈ S`), then the fraction `r /ₒ s` is equal to `r * t /ₒ (s * t)`. The notation `/ₒ` represents the localized division in the ring of fractions, where `s` and `s * t` are considered as elements of `S`.
More concisely: For any Monoid `R`, submonoid `S`, and elements `r` in `R`, `s` in `S`, and `t` in `R` such that `s * t` is in `S`, the localized division `r /ₒ s` equals `r * t /ₒ (s * t)`.
|
OreLocalization.zero_def
theorem OreLocalization.zero_def :
∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S], 0 = 0 /ₒ 1
This theorem, `OreLocalization.zero_def`, states that for every type `R` that is a semiring and for every submonoid `S` of `R` that is an Ore set, the value of zero in the Ore localization is equal to the fraction `0 /ₒ 1`. In other words, in the context of Ore localization, zero can be expressed as the ratio of zero to one.
More concisely: In an Ore localization of a semiring R with respect to an Ore set S, the element representing zero is equal to the fraction 0 /ₒ 1.
|
OreLocalization.zero_div_eq_zero
theorem OreLocalization.zero_div_eq_zero :
∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (s : ↥S), 0 /ₒ s = 0
This theorem states that for any type `R` that has a `Semiring` structure and any `S` which is a submonoid of `R`, if `S` is also an `OreLocalization.OreSet`, then the division of zero by any element `s` in `S` (notated as `0 /ₒ s`) is equal to zero. Essentially, it's stating that in this specific algebraic setting, division of zero by any non-zero element results in zero, mirroring a common property in ordinary division.
More concisely: For any semiring `R` and submonoid `S` of `R` that is an `OreLocalization.OreSet`, the division of zero by any element `s` in `S`, `0 /ₒ s`, equals zero.
|
OreLocalization.one_def
theorem OreLocalization.one_def :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S], 1 = 1 /ₒ 1
This theorem states that in the context of Ore localization, given any type `R` which forms a monoid and a submonoid `S` of `R` that is an Ore set, the identity element '1' of the Ore localization is equal to the fraction '1 over 1' in the Ore localization. The Ore localization is a method of generalizing the construction of the quotient field of an integral domain to more general rings.
More concisely: In the context of Ore localization, the identity element is equal to '1/1' in the Ore localization of a monoid `R` with an Ore submonoid `S`.
|
OreLocalization.universalMulHom_unique
theorem OreLocalization.universalMulHom_unique :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_2}
[inst_2 : Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : OreLocalization R S →* T),
(∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) → φ = OreLocalization.universalMulHom f fS hf
The theorem `OreLocalization.universalMulHom_unique` states that given a monoid `R`, a submonoid `S` of `R` satisfying the Ore condition, and another monoid `T`, for a multiplicative homomorphism `f` from `R` to `T` and a function `fS` mapping elements of `S` to units of `T` such that `f` applied to any element of `S` is equal to `fS` applied to the same element, the universal morphism `universalMulHom` that lifts `f` to a morphism from the Ore localization of `R` at `S` to `T` is unique. Specifically, if there is another morphism `φ` from the Ore localization of `R` at `S` to `T` such that `φ` applied to any element `r` of `R` under the `numeratorHom` is equal to `f` applied to `r`, then `φ` must be equal to `universalMulHom` applied to `f`, `fS`, and the condition `hf`. In other words, any morphism that agrees with `f` at the elements of `R` must be the universal lifting of `f`.
More concisely: Given a monoid `R`, a submonoid `S` of `R` satisfying the Ore condition, a monoid `T`, a multiplicative homomorphism `f` from `R` to `T`, and a function `fS` mapping elements of `S` to units of `T` such that `f(s) = fS(s)` for all `s` in `S`, the universal morphism from the Ore localization of `R` at `S` to `T` lifting `f` is unique.
|
OreLocalization.oreDiv_add_char
theorem OreLocalization.oreDiv_add_char :
∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r r' : R} (s s' : ↥S)
(rb : R) (sb : ↥S), ↑s * ↑sb = ↑s' * rb → r /ₒ s + r' /ₒ s' = (r * ↑sb + r' * rb) /ₒ (s * sb)
This theorem provides a characterization of addition in the Ore localization of a semiring. For any semiring `R`, given elements `r`, `r'` of `R`, and `s`, `s'`, `sb` in the submonoid `S`, and `rb` in `R`, if `s * sb = s' * rb` holds, it states that the sum of the Ore fractions `r /ₒ s` and `r' /ₒ s'` is equal to the Ore fraction `(r * sb + r' * rb) /ₒ (s * sb)`.
More concisely: For any semiring `R` and elements `r`, `r'` of `R` and `s`, `s'`, `sb` in its submonoid, if `s * sb = s' * rb` holds, then `(r /ₒ s) + (r' /ₒ s') = (r * sb + r' * rb) /ₒ (s * sb)`.
|
OreLocalization.numeratorHom_apply
theorem OreLocalization.numeratorHom_apply :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r : R},
OreLocalization.numeratorHom r = r /ₒ 1
The theorem `OreLocalization.numeratorHom_apply` states that for any type `R` that forms a monoid, any submonoid `S` of `R` that serves as an Ore localization set, and any element `r` from `R`, the application of the Ore localization numerator homomorphism on `r` results in the fraction `r /ₒ 1`. This expresses the action of the Ore localization numerator homomorphism as creating fractions where the denominator is `1`.
More concisely: For any monoid `R`, submonoid `S` serving as an Ore localization set, and `r` in `R`, the Ore localization numerator homomorphism applied to `r` equals `r /ₒ 1`.
|
OreLocalization.eq_of_num_factor_eq
theorem OreLocalization.eq_of_num_factor_eq :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r r' r₁ r₂ : R}
{s t : ↥S}, r * ↑t = r' * ↑t → r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
This theorem, named `OreLocalization.eq_of_num_factor_eq`, asserts that in the context of a monoid `R` and a submonoid `S` of `R` that satisfies the Ore condition (an abstraction of the localization of a ring), if two fractions have numerators `r` and `r'` that differ by a factor of `↑t`, where `t` is a member of the submonoid `S`, then those fractions are equal as long as they have the same denominator `s`. More specifically, if `r * ↑t = r' * ↑t`, then `r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s`, where `r₁` and `r₂` are elements of `R`.
More concisely: If `r` and `r'` are elements of a monoid `R` with submonoid `S` satisfying the Ore condition, and `r * ↑t = r' * ↑t` for some `t ∈ S`, then `r * s /ₒ t = r' * s /ₒ t` for any `s ∈ R`.
|
OreLocalization.expand'
theorem OreLocalization.expand' :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s s' : ↥S),
r /ₒ s = r * ↑s' /ₒ (s * s')
This theorem, named `OreLocalization.expand'`, states that for any type `R` that forms a Monoid, and a Submonoid `S` of `R` that satisfies the Ore condition, a fraction formed by a member `r` of `R` and a member `s` of `S` is equal to the fraction formed by `r` times a member `s'` of `S` and the product of `s` and `s'`. Here, `/ₒ` denotes the Ore localization of `R` at `S`, and `*` denotes the multiplication operation of the Monoid. The symbols `↑s'` and `(s * s')` serve to embed `s'` and the product `s * s'` into the Ore localization.
More concisely: For any Monoid `R` and Submonoid `S` of `R` satisfying the Ore condition, the fraction `r / s` in the Ore localization of `R` at `S` equals `r * s' / (s * s')` for any `r` in `R` and `s'` in `S`.
|