(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} [Monoid R] (S : Submonoid R) : 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 : R → ↥S → R

  The Ore numerator of a fraction.

• oreDenom : R → ↥S → ↥S

  The Ore denominator of a fraction.

• ore_eq : ∀ (r : R) (s : ↥S), r * ↑(OreLocalization.OreSet.oreDenom r s) = ↑s * OreLocalization.OreSet.oreNum r s

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

theorem OreLocalization.ore_left_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet 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} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : ↥S) : R

The Ore numerator of a fraction.

Equations

• OreLocalization.oreNum r s = OreLocalization.OreSet.oreNum r s

def OreLocalization.oreDenom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : ↥S) : ↥S

The Ore denominator of a fraction.

Equations

• OreLocalization.oreDenom r s = OreLocalization.OreSet.oreDenom r s

theorem OreLocalization.ore_eq {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : ↥S) : r * ↑(OreLocalization.oreDenom r s) = ↑s * OreLocalization.oreNum r s

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

def OreLocalization.oreCondition {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet 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

• OreLocalization.oreCondition r s = { fst := OreLocalization.oreNum r s, snd := { fst := OreLocalization.oreDenom r s, snd := ⋯ } }

instance OreLocalization.oreSetBot {R : Type u_1} [Monoid R] : OreLocalization.OreSet ⊥

The trivial submonoid is an Ore set.

Equations

• OreLocalization.oreSetBot = { ore_left_cancel := ⋯, oreNum := fun (r : R) (x : ↥⊥) => r, oreDenom := fun (x : R) (s : ↥⊥) => s, ore_eq := ⋯ }

instance OreLocalization.oreSetComm {R : Type u_2} [CommMonoid R] (S : Submonoid R) : OreLocalization.OreSet S

Every submonoid of a commutative monoid is an Ore set.

Equations

• OreLocalization.oreSetComm S = { ore_left_cancel := ⋯, oreNum := fun (r : R) (x : ↥S) => r, oreDenom := fun (x : R) (s : ↥S) => s, ore_eq := ⋯ }

def OreLocalization.oreSetOfCancelMonoidWithZero {R : Type u_1} [CancelMonoidWithZero R] {S : Submonoid R} (oreNum : R → ↥S → R) (oreDenom : R → ↥S → ↥S) (ore_eq : ∀ (r : R) (s : ↥S), r * ↑(oreDenom r s) = ↑s * oreNum r s) : OreLocalization.OreSet S

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

Equations

• OreLocalization.oreSetOfCancelMonoidWithZero oreNum oreDenom ore_eq = { ore_left_cancel := ⋯, oreNum := oreNum, oreDenom := oreDenom, ore_eq := ore_eq }

def OreLocalization.oreSetOfNoZeroDivisors {R : Type u_1} [Ring R] [NoZeroDivisors R] {S : Submonoid R} (oreNum : R → ↥S → R) (oreDenom : R → ↥S → ↥S) (ore_eq : ∀ (r : R) (s : ↥S), r * ↑(oreDenom r s) = ↑s * oreNum r s) : OreLocalization.OreSet 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

• OreLocalization.oreSetOfNoZeroDivisors oreNum oreDenom ore_eq = OreLocalization.oreSetOfCancelMonoidWithZero oreNum oreDenom ore_eq

theorem OreLocalization.nonempty_oreSet_iff {R : Type u_1} [Ring R] {S : Submonoid R} : Nonempty (OreLocalization.OreSet S) ↔ (∀ (r₁ r₂ : R) (s : ↥S), ↑s * r₁ = ↑s * r₂ → ∃ (s' : ↥S), r₁ * ↑s' = r₂ * ↑s') ∧ ∀ (r : R) (s : ↥S), ∃ (r' : R) (s' : ↥S), r * ↑s' = ↑s * r'

theorem OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors {R : Type u_1} [Ring R] [NoZeroDivisors R] {S : Submonoid R} : Nonempty (OreLocalization.OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ (r' : R) (s' : ↥S), r * ↑s' = ↑s * r'