# (Right) Ore sets #

This defines right Ore sets on arbitrary monoids.

## References #

• https://ncatlab.org/nlab/show/Ore+set
class OreLocalization.OreSet {R : Type u_1} [] (S : ) :
Type u_1

A submonoid S of a monoid R is (right) Ore if common factors on the left can be turned into common factors on the right, and if each pair of r : R and s : S admits an Ore numerator v : R and an Ore denominator u : S such that r * u = s * v.

• ore_left_cancel : ∀ (r₁ r₂ : R) (s : S), s * r₁ = s * r₂∃ (s' : S), r₁ * s' = r₂ * s'

Common factors on the left can be turned into common factors on the right, a weak form of cancellability.

• oreNum : RSR

The Ore numerator of a fraction.

The Ore denominator of a fraction.

• ore_eq : ∀ (r : R) (s : S), r * =

The Ore condition of a fraction, expressed in terms of oreNum and oreDenom.

Instances
theorem OreLocalization.ore_left_cancel {R : Type u_1} [] {S : } (r₁ : R) (r₂ : R) (s : S) (h : s * r₁ = s * r₂) :
∃ (s' : S), r₁ * s' = r₂ * s'

Common factors on the left can be turned into common factors on the right, a weak form of cancellability.

def OreLocalization.oreNum {R : Type u_1} [] {S : } (r : R) (s : S) :
R

The Ore numerator of a fraction.

Equations
Instances For
def OreLocalization.oreDenom {R : Type u_1} [] {S : } (r : R) (s : S) :
S

The Ore denominator of a fraction.

Equations
Instances For
theorem OreLocalization.ore_eq {R : Type u_1} [] {S : } (r : R) (s : S) :
r * () = s *

The Ore condition of a fraction, expressed in terms of oreNum and oreDenom.

def OreLocalization.oreCondition {R : Type u_1} [] {S : } (r : R) (s : S) :
(r' : R) ×' (s' : S) ×' r * s' = s * r'

The Ore condition bundled in a sigma type. This is useful in situations where we want to obtain both witnesses and the condition for a given fraction.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance OreLocalization.oreSetBot {R : Type u_1} [] :

The trivial submonoid is an Ore set.

Equations
• One or more equations did not get rendered due to their size.
instance OreLocalization.oreSetComm {R : Type u_2} [] (S : ) :

Every submonoid of a commutative monoid is an Ore set.

Equations
• One or more equations did not get rendered due to their size.
def OreLocalization.oreSetOfCancelMonoidWithZero {R : Type u_1} {S : } (oreNum : RSR) (oreDenom : RSS) (ore_eq : ∀ (r : R) (s : S), r * (oreDenom r s) = s * oreNum r s) :

Cancellability in monoids with zeros can act as a replacement for the ore_left_cancel condition of an ore set.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def OreLocalization.oreSetOfNoZeroDivisors {R : Type u_1} [Ring R] [] {S : } (oreNum : RSR) (oreDenom : RSS) (ore_eq : ∀ (r : R) (s : S), r * (oreDenom r s) = s * oreNum r s) :

In rings without zero divisors, the first (cancellability) condition is always fulfilled, it suffices to give a proof for the Ore condition itself.

Equations
Instances For