Localization over right Ore sets. #
This file defines the localization of a monoid over a right Ore set and proves its universal
mapping property. It then extends the definition and its properties first to semirings and then
to rings. We show that in the case of a commutative monoid this definition coincides with the
common monoid localization. Finally we show that in a ring without zero divisors, taking the Ore
localization at R - {0} results in a division ring.
Notations #
Introduces the notation R[S⁻¹] for the Ore localization of a monoid R at a right Ore
subset S. Also defines a new heterogeneous division notation r /ₒ s for a numerator r : R and
a denominator s : S.
References #
- https://ncatlab.org/nlab/show/Ore+localization
- [Zoran Škoda, Noncommutative localization in noncommutative geometry][skoda2006]
Tags #
localization, Ore, non-commutative
The setoid on R × S used for the Ore localization.
Instances For
def
OreLocalization
(R : Type u_1)
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
:
Type u_1
The ore localization of a monoid and a submonoid fulfilling the ore condition.
Instances For
The ore localization of a monoid and a submonoid fulfilling the ore condition.
Instances For
def
OreLocalization.oreDiv
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(r : R)
(s : { x // x ∈ S })
:
OreLocalization R S
The division in the ore localization R[S⁻¹], as a fraction of an element of R and S.
Instances For
The division in the ore localization R[S⁻¹], as a fraction of an element of R and S.
Instances For
theorem
OreLocalization.ind
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{β : OreLocalization R S → Prop}
(c : (r : R) → (s : { x // x ∈ S }) → β (r /ₒ s))
(q : OreLocalization R S)
:
β q
theorem
OreLocalization.eq_of_num_factor_eq
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r : R}
{r' : R}
{r₁ : R}
{r₂ : R}
{s : { x // x ∈ S }}
{t : { x // x ∈ S }}
(h : r * ↑t = r' * ↑t)
:
Fractions which differ by a factor of the numerator can be proven equal if
those factors expand to equal elements of R.
def
OreLocalization.liftExpand
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{C : Sort u_2}
(P : R → { x // x ∈ S } → C)
(hP : ∀ (r t : R) (s : { x // x ∈ S }) (ht : ↑s * t ∈ S), P r s = P (r * t) { val := ↑s * t, property := ht })
:
OreLocalization R S → C
A function or predicate over R and S can be lifted to R[S⁻¹] if it is invariant
under expansion on the right.
Instances For
@[simp]
theorem
OreLocalization.liftExpand_of
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{C : Sort u_2}
{P : R → { x // x ∈ S } → C}
{hP : ∀ (r t : R) (s : { x // x ∈ S }) (ht : ↑s * t ∈ S), P r s = P (r * t) { val := ↑s * t, property := ht }}
(r : R)
(s : { x // x ∈ S })
:
OreLocalization.liftExpand P hP (r /ₒ s) = P r s
def
OreLocalization.lift₂Expand
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{C : Sort u_2}
(P : R → { x // x ∈ S } → R → { x // x ∈ S } → C)
(hP : ∀ (r₁ t₁ : R) (s₁ : { x // x ∈ S }) (ht₁ : ↑s₁ * t₁ ∈ S) (r₂ t₂ : R) (s₂ : { x // x ∈ S }) (ht₂ : ↑s₂ * t₂ ∈ S),
P r₁ s₁ r₂ s₂ = P (r₁ * t₁) { val := ↑s₁ * t₁, property := ht₁ } (r₂ * t₂) { val := ↑s₂ * t₂, property := ht₂ })
:
OreLocalization R S → OreLocalization R S → C
A version of liftExpand used to simultaneously lift functions with two arguments
in R[S⁻¹].
Instances For
@[simp]
theorem
OreLocalization.lift₂Expand_of
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{C : Sort u_2}
{P : R → { x // x ∈ S } → R → { x // x ∈ S } → C}
{hP : ∀ (r₁ t₁ : R) (s₁ : { x // x ∈ S }) (ht₁ : ↑s₁ * t₁ ∈ S) (r₂ t₂ : R) (s₂ : { x // x ∈ S }) (ht₂ : ↑s₂ * t₂ ∈ S),
P r₁ s₁ r₂ s₂ = P (r₁ * t₁) { val := ↑s₁ * t₁, property := ht₁ } (r₂ * t₂) { val := ↑s₂ * t₂, property := ht₂ }}
(r₁ : R)
(s₁ : { x // x ∈ S })
(r₂ : R)
(s₂ : { x // x ∈ S })
:
OreLocalization.lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂
def
OreLocalization.mul
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
OreLocalization R S → OreLocalization R S → OreLocalization R S
The multiplication on the Ore localization of monoids.
Instances For
instance
OreLocalization.instMulOreLocalization
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Mul (OreLocalization R S)
theorem
OreLocalization.oreDiv_mul_oreDiv
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r₁ : R}
{r₂ : R}
{s₁ : { x // x ∈ S }}
{s₂ : { x // x ∈ S }}
:
r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * OreLocalization.oreNum r₂ s₁ /ₒ (s₂ * OreLocalization.oreDenom r₂ s₁)
theorem
OreLocalization.oreDiv_mul_char
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(r₁ : R)
(r₂ : R)
(s₁ : { x // x ∈ S })
(s₂ : { x // x ∈ S })
(r' : R)
(s' : { x // x ∈ S })
(huv : r₂ * ↑s' = ↑s₁ * r')
:
A characterization lemma for the multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.
def
OreLocalization.oreDivMulChar'
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(r₁ : R)
(r₂ : R)
(s₁ : { x // x ∈ S })
(s₂ : { x // x ∈ S })
:
Another characterization lemma for the multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.
Instances For
instance
OreLocalization.instOneOreLocalization
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
One (OreLocalization R S)
theorem
OreLocalization.one_def
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
instance
OreLocalization.instInhabitedOreLocalization
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Inhabited (OreLocalization R S)
@[simp]
theorem
OreLocalization.div_eq_one'
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r : R}
(hr : r ∈ S)
:
@[simp]
theorem
OreLocalization.div_eq_one
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{s : { x // x ∈ S }}
:
theorem
OreLocalization.one_mul
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
:
theorem
OreLocalization.mul_one
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
:
theorem
OreLocalization.mul_assoc
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
(y : OreLocalization R S)
(z : OreLocalization R S)
:
instance
OreLocalization.instMonoidOreLocalization
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Monoid (OreLocalization R S)
def
OreLocalization.numeratorUnit
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(s : { x // x ∈ S })
:
(OreLocalization R S)ˣ
The fraction s /ₒ 1 as a unit in R[S⁻¹], where s : S.
Instances For
def
OreLocalization.numeratorHom
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
R →* OreLocalization R S
The multiplicative homomorphism from R to R[S⁻¹], mapping r : R to the
fraction r /ₒ 1.
Instances For
theorem
OreLocalization.numeratorHom_apply
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r : R}
:
theorem
OreLocalization.numerator_isUnit
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(s : { x // x ∈ S })
:
IsUnit (↑OreLocalization.numeratorHom ↑s)
def
OreLocalization.universalMulHom
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Monoid T]
(f : R →* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
:
OreLocalization R S →* T
The universal lift from a morphism R →* T, which maps elements of S to units of T,
to a morphism R[S⁻¹] →* T.
Instances For
theorem
OreLocalization.universalMulHom_apply
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Monoid T]
(f : R →* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
{r : R}
{s : { x // x ∈ S }}
:
↑(OreLocalization.universalMulHom f fS hf) (r /ₒ s) = ↑f r * ↑(↑fS s)⁻¹
theorem
OreLocalization.universalMulHom_commutes
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Monoid T]
(f : R →* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
{r : R}
:
↑(OreLocalization.universalMulHom f fS hf) (↑OreLocalization.numeratorHom r) = ↑f r
theorem
OreLocalization.universalMulHom_unique
{R : Type u_1}
[Monoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Monoid T]
(f : R →* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
(φ : OreLocalization R S →* T)
(huniv : ∀ (r : R), ↑φ (↑OreLocalization.numeratorHom r) = ↑f r)
:
φ = OreLocalization.universalMulHom f fS hf
The universal morphism universalMulHom is unique.
theorem
OreLocalization.oreDiv_mul_oreDiv_comm
{R : Type u_1}
[CommMonoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r₁ : R}
{r₂ : R}
{s₁ : { x // x ∈ S }}
{s₂ : { x // x ∈ S }}
:
instance
OreLocalization.instCommMonoidOreLocalizationToMonoid
{R : Type u_1}
[CommMonoid R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
CommMonoid (OreLocalization R S)
def
OreLocalization.localizationMap
(R : Type u_1)
[CommMonoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
:
The morphism numeratorHom is a monoid localization map in the case of commutative R.
Instances For
noncomputable def
OreLocalization.equivMonoidLocalization
(R : Type u_1)
[CommMonoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
:
Localization S ≃* OreLocalization R S
If R is commutative, Ore localization and monoid localization are isomorphic.
Instances For
instance
OreLocalization.instAddOreLocalization
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Add (OreLocalization R S)
theorem
OreLocalization.oreDiv_add_oreDiv
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r : R}
{r' : R}
{s : { x // x ∈ S }}
{s' : { x // x ∈ S }}
:
r /ₒ s + r' /ₒ s' = (r * ↑(OreLocalization.oreDenom (↑s) s') + r' * OreLocalization.oreNum (↑s) s') /ₒ (s * OreLocalization.oreDenom (↑s) s')
theorem
OreLocalization.oreDiv_add_char
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{r : R}
{r' : R}
(s : { x // x ∈ S })
(s' : { x // x ∈ S })
(rb : R)
(sb : { x // x ∈ S })
(h : ↑s * ↑sb = ↑s' * rb)
:
A characterization of the addition on the Ore localizaion, allowing for arbitrary Ore numerator and Ore denominator.
def
OreLocalization.oreDivAddChar'
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(r : R)
(r' : R)
(s : { x // x ∈ S })
(s' : { x // x ∈ S })
:
Another characterization of the addition on the Ore localization, bundling up all witnesses and conditions into a sigma type.
Instances For
theorem
OreLocalization.add_assoc
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
(y : OreLocalization R S)
(z : OreLocalization R S)
:
instance
OreLocalization.instZeroOreLocalizationToMonoidToMonoidWithZero
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Zero (OreLocalization R S)
theorem
OreLocalization.zero_def
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
@[simp]
theorem
OreLocalization.zero_div_eq_zero
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(s : { x // x ∈ S })
:
theorem
OreLocalization.zero_add
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
:
theorem
OreLocalization.add_comm
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
(y : OreLocalization R S)
:
instance
OreLocalization.instAddCommMonoidOreLocalization
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
AddCommMonoid (OreLocalization R S)
theorem
OreLocalization.zero_mul
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
:
theorem
OreLocalization.mul_zero
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
:
theorem
OreLocalization.left_distrib
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
(y : OreLocalization R S)
(z : OreLocalization R S)
:
theorem
OreLocalization.right_distrib
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
(y : OreLocalization R S)
(z : OreLocalization R S)
:
instance
OreLocalization.instSemiringOreLocalization
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Semiring (OreLocalization R S)
def
OreLocalization.universalHom
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Semiring T]
(f : R →+* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
:
OreLocalization R S →+* T
The universal lift from a ring homomorphism f : R →+* T, which maps elements in S to
units of T, to a ring homomorphism R[S⁻¹] →+* T. This extends the construction on
monoids.
Instances For
theorem
OreLocalization.universalHom_apply
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Semiring T]
(f : R →+* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
{r : R}
{s : { x // x ∈ S }}
:
↑(OreLocalization.universalHom f fS hf) (r /ₒ s) = ↑f r * ↑(↑fS s)⁻¹
theorem
OreLocalization.universalHom_commutes
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Semiring T]
(f : R →+* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
{r : R}
:
↑(OreLocalization.universalHom f fS hf) (↑OreLocalization.numeratorHom r) = ↑f r
theorem
OreLocalization.universalHom_unique
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
{T : Type u_2}
[Semiring T]
(f : R →+* T)
(fS : { x // x ∈ S } →* Tˣ)
(hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s))
(φ : OreLocalization R S →+* T)
(huniv : ∀ (r : R), ↑φ (↑OreLocalization.numeratorHom r) = ↑f r)
:
φ = OreLocalization.universalHom f fS hf
def
OreLocalization.neg
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
OreLocalization R S → OreLocalization R S
Negation on the Ore localization is defined via negation on the numerator.
Instances For
instance
OreLocalization.instNegOreLocalization
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Neg (OreLocalization R S)
theorem
OreLocalization.add_left_neg
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization R S)
:
instance
OreLocalization.ring
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Ring (OreLocalization R S)
theorem
OreLocalization.numeratorHom_inj
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(hS : S ≤ nonZeroDivisors R)
:
Function.Injective ↑OreLocalization.numeratorHom
theorem
OreLocalization.nontrivial_of_nonZeroDivisors
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
[Nontrivial R]
(hS : S ≤ nonZeroDivisors R)
:
Nontrivial (OreLocalization R S)
instance
OreLocalization.nontrivial
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
:
Nontrivial (OreLocalization R (nonZeroDivisors R))
def
OreLocalization.inv
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
:
OreLocalization R (nonZeroDivisors R) → OreLocalization R (nonZeroDivisors R)
The inversion of Ore fractions for a ring without zero divisors, satisying 0⁻¹ = 0 and
(r /ₒ r')⁻¹ = r' /ₒ r for r ≠ 0.
Instances For
instance
OreLocalization.inv'
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
:
Inv (OreLocalization R (nonZeroDivisors R))
theorem
OreLocalization.inv_def
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
{r : R}
{s : { x // x ∈ nonZeroDivisors R }}
:
theorem
OreLocalization.mul_inv_cancel
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
(x : OreLocalization R (nonZeroDivisors R))
(h : x ≠ 0)
:
theorem
OreLocalization.inv_zero
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
:
instance
OreLocalization.divisionRing
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
: