(Left) Ore sets

This defines left Ore sets on arbitrary monoids.

References

• https://ncatlab.org/nlab/show/Ore+set

class AddOreLocalization.AddOreSet {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) : Type u_1

A submonoid S of an additive monoid R is (left) Ore if common summands on the right can be turned into common summands on the left, and if each pair of r : R and s : S admits an Ore minuend v : R and an Ore subtrahend u : S such that u + r = v + s.

• ore_right_cancel : ∀ (r₁ r₂ : R) (s : { x : R // x ∈ S }), r₁ + ↑s = r₂ + ↑s → ∃ (s' : { x : R // x ∈ S }), ↑s' + r₁ = ↑s' + r₂

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

• oreMin : R → { x : R // x ∈ S } → R

  The Ore minuend of a difference.

• oreSubtra : R → { x : R // x ∈ S } → { x : R // x ∈ S }

  The Ore subtrahend of a difference.

• ore_eq : ∀ (r : R) (s : { x : R // x ∈ S }), ↑(AddOreLocalization.AddOreSet.oreSubtra r s) + r = AddOreLocalization.AddOreSet.oreMin r s + ↑s

  The Ore condition of a difference, expressed in terms of oreMin and oreSubtra.

theorem AddOreLocalization.AddOreSet.ore_right_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [self : AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s : { x : R // x ∈ S }) : r₁ + ↑s = r₂ + ↑s → ∃ (s' : { x : R // x ∈ S }), ↑s' + r₁ = ↑s' + r₂

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

theorem AddOreLocalization.AddOreSet.ore_eq {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [self : AddOreLocalization.AddOreSet S] (r : R) (s : { x : R // x ∈ S }) : ↑(AddOreLocalization.AddOreSet.oreSubtra r s) + r = AddOreLocalization.AddOreSet.oreMin r s + ↑s

The Ore condition of a difference, expressed in terms of oreMin and oreSubtra.

class OreLocalization.OreSet {R : Type u_1} [Monoid R] (S : Submonoid R) : Type u_1

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

• ore_right_cancel : ∀ (r₁ r₂ : R) (s : { x : R // x ∈ S }), r₁ * ↑s = r₂ * ↑s → ∃ (s' : { x : R // x ∈ S }), ↑s' * r₁ = ↑s' * r₂

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

• oreNum : R → { x : R // x ∈ S } → R

  The Ore numerator of a fraction.

• oreDenom : R → { x : R // x ∈ S } → { x : R // x ∈ S }

  The Ore denominator of a fraction.

• ore_eq : ∀ (r : R) (s : { x : R // x ∈ S }), ↑(OreLocalization.OreSet.oreDenom r s) * r = OreLocalization.OreSet.oreNum r s * ↑s

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

theorem OreLocalization.OreSet.ore_right_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [self : OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s : { x : R // x ∈ S }) : r₁ * ↑s = r₂ * ↑s → ∃ (s' : { x : R // x ∈ S }), ↑s' * r₁ = ↑s' * r₂

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

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

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

theorem AddOreLocalization.ore_right_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s : { x : R // x ∈ S }) (h : r₁ + ↑s = r₂ + ↑s) : ∃ (s' : { x : R // x ∈ S }), ↑s' + r₁ = ↑s' + r₂

theorem OreLocalization.ore_right_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s : { x : R // x ∈ S }) (h : r₁ * ↑s = r₂ * ↑s) : ∃ (s' : { x : R // x ∈ S }), ↑s' * r₁ = ↑s' * r₂

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

def AddOreLocalization.oreMin {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r : R) (s : { x : R // x ∈ S }) : R

The Ore minuend of a difference.

Equations

• AddOreLocalization.oreMin r s = AddOreLocalization.AddOreSet.oreMin r s

def OreLocalization.oreNum {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : { x : R // x ∈ S }) : R

The Ore numerator of a fraction.

Equations

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

def AddOreLocalization.oreSubtra {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r : R) (s : { x : R // x ∈ S }) : { x : R // x ∈ S }

The Ore subtrahend of a difference.

Equations

• AddOreLocalization.oreSubtra r s = AddOreLocalization.AddOreSet.oreSubtra r s

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

The Ore denominator of a fraction.

Equations

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

theorem AddOreLocalization.add_ore_eq {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r : R) (s : { x : R // x ∈ S }) : ↑(AddOreLocalization.oreSubtra r s) + r = AddOreLocalization.oreMin r s + ↑s

The Ore condition of a difference, expressed in terms of oreMin and oreSubtra.

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

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

def AddOreLocalization.addOreCondition {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r : R) (s : { x : R // x ∈ S }) : (r' : R) ×' (s' : { x : R // x ∈ S }) ×' ↑s' + r = r' + ↑s

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 difference.

Equations

• AddOreLocalization.addOreCondition r s = ⟨AddOreLocalization.oreMin r s, ⟨AddOreLocalization.oreSubtra r s, ⋯⟩⟩

def OreLocalization.oreCondition {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : { x : R // x ∈ S }) : (r' : R) ×' (s' : { x : R // x ∈ S }) ×' ↑s' * r = r' * ↑s

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 = ⟨OreLocalization.oreNum r s, ⟨OreLocalization.oreDenom r s, ⋯⟩⟩

instance AddOreLocalization.addOreSetBot {R : Type u_1} [AddMonoid R] : AddOreLocalization.AddOreSet ⊥

Equations

• AddOreLocalization.addOreSetBot = { ore_right_cancel := ⋯, oreMin := fun (r : R) (x : { x : R // x ∈ ⊥ }) => r, oreSubtra := fun (x : R) (s : { x : R // x ∈ ⊥ }) => s, ore_eq := ⋯ }

theorem AddOreLocalization.addOreSetBot.proof_1 {R : Type u_1} [AddMonoid R] : ∀ (x x_1 : R) (s : { x : R // x ∈ ⊥ }), x + ↑s = x_1 + ↑s → ∃ (s' : { x : R // x ∈ ⊥ }), ↑s' + x = ↑s' + x_1

theorem AddOreLocalization.addOreSetBot.proof_2 {R : Type u_1} [AddMonoid R] : ∀ (x : R) (s : { x : R // x ∈ ⊥ }), ↑((fun (x : R) (s : { x : R // x ∈ ⊥ }) => s) x s) + x = (fun (r : R) (x : { x : R // x ∈ ⊥ }) => r) x s + ↑s

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

The trivial submonoid is an Ore set.

Equations

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

theorem AddOreLocalization.addOreSetComm.proof_1 {R : Type u_1} [AddCommMonoid R] (S : AddSubmonoid R) (m : R) (n : R) (s : { x : R // x ∈ S }) (h : m + ↑s = n + ↑s) : ∃ (s' : { x : R // x ∈ S }), ↑s' + m = ↑s' + n

theorem AddOreLocalization.addOreSetComm.proof_2 {R : Type u_1} [AddCommMonoid R] (S : AddSubmonoid R) (r : R) (s : { x : R // x ∈ S }) : ↑((fun (x : R) (s : { x : R // x ∈ S }) => s) r s) + r = (fun (r : R) (x : { x : R // x ∈ S }) => r) r s + ↑s

@[instance 100]

instance AddOreLocalization.addOreSetComm {R : Type u_2} [AddCommMonoid R] (S : AddSubmonoid R) : AddOreLocalization.AddOreSet S

Equations

• AddOreLocalization.addOreSetComm S = { ore_right_cancel := ⋯, oreMin := fun (r : R) (x : { x : R // x ∈ S }) => r, oreSubtra := fun (x : R) (s : { x : R // x ∈ S }) => s, ore_eq := ⋯ }

@[instance 100]

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_right_cancel := ⋯, oreNum := fun (r : R) (x : { x : R // x ∈ S }) => r, oreDenom := fun (x : R) (s : { x : R // x ∈ S }) => s, ore_eq := ⋯ }

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

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

Equations

• OreLocalization.oreSetOfCancelMonoidWithZero oreNum oreDenom ore_eq = { ore_right_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 → { x : R // x ∈ S } → R) (oreDenom : R → { x : R // x ∈ S } → { x : R // x ∈ S }) (ore_eq : ∀ (r : R) (s : { x : R // x ∈ S }), ↑(oreDenom r s) * r = oreNum r s * ↑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 : { x : R // x ∈ S }), r₁ * ↑s = r₂ * ↑s → ∃ (s' : { x : R // x ∈ S }), ↑s' * r₁ = ↑s' * r₂) ∧ ∀ (r : R) (s : { x : R // x ∈ S }), ∃ (r' : R) (s' : { x : R // x ∈ S }), ↑s' * r = r' * ↑s

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 : { x : R // x ∈ S }), ∃ (r' : R) (s' : { x : R // x ∈ S }), ↑s' * r = r' * ↑s