(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 : ↥S) : r₁ + ↑s = r₂ + ↑s → ∃ (s' : ↥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 → ↥S → R

  The Ore minuend of a difference.

• oreSubtra : R → ↥S → ↥S

  The Ore subtrahend of a difference.

• ore_eq (r : R) (s : ↥S) : ↑(oreSubtra r s) + r = 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 : ↥S) : r₁ * ↑s = r₂ * ↑s → ∃ (s' : ↥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 → ↥S → R

  The Ore numerator of a fraction.

• oreDenom : R → ↥S → ↥S

  The Ore denominator of a fraction.

• ore_eq (r : R) (s : ↥S) : ↑(oreDenom r s) * r = oreNum r s * ↑s

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

theorem OreLocalization.ore_right_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (r₁ r₂ : R) (s : ↥S) (h : r₁ * ↑s = r₂ * ↑s) : ∃ (s' : ↥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 AddOreLocalization.ore_right_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (r₁ r₂ : R) (s : ↥S) (h : r₁ + ↑s = r₂ + ↑s) : ∃ (s' : ↥S), ↑s' + r₁ = ↑s' + r₂

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

The Ore numerator of a fraction.

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

The Ore minuend of a difference.

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

The Ore denominator of a fraction.

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

The Ore subtrahend of a difference.

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

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

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

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

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

def AddOreLocalization.addOreCondition {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (r : R) (s : ↥S) : (r' : R) ×' (s' : ↥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.

@[implicit_reducible]

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

The trivial submonoid is an Ore set.

@[implicit_reducible]

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

@[implicit_reducible, instance 100]

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

Every submonoid of a commutative monoid is an Ore set.

@[implicit_reducible, instance 100]

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

@[simp]

theorem OreLocalization.oreSetComm_oreNum {R : Type u_2} [CommMonoid R] (S : Submonoid R) (r : R) (s : ↥S) : oreNum r s = r

@[simp]

theorem AddOreLocalization.addOreSetComm_oreMin {R : Type u_2} [AddCommMonoid R] (S : AddSubmonoid R) (r : R) (s : ↥S) : oreMin r s = r

@[simp]

theorem OreLocalization.oreSetComm_oreDenom {R : Type u_2} [CommMonoid R] (S : Submonoid R) (r : R) (s : ↥S) : oreDenom r s = s

@[simp]

theorem AddOreLocalization.addOreSetComm_oreSubtra {R : Type u_2} [AddCommMonoid R] (S : AddSubmonoid R) (r : R) (s : ↥S) : oreSubtra r s = s