# (Left) Ore sets #

This defines left Ore sets on arbitrary monoids.

## References #

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

source
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`.

Instances

source
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`.

Instances

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

source
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₂
source
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.

Equations

- OreLocalization.oreNum r s = OreLocalization.OreSet.oreNum r s

Instances For

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

Equations

- AddOreLocalization.oreMin r s = AddOreLocalization.AddOreSet.oreMin r s

Instances For

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

Equations

- OreLocalization.oreDenom r s = OreLocalization.OreSet.oreDenom r s

Instances For

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

Equations

- AddOreLocalization.oreSubtra r s = AddOreLocalization.AddOreSet.oreSubtra r s

Instances For

source
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`.

source
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`.

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

Equations

- OreLocalization.oreCondition r s = ⟨OreLocalization.oreNum r s, ⟨OreLocalization.oreDenom r s, ⋯⟩⟩

Instances For

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

Equations

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

Instances For

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

The trivial submonoid is an Ore set.

Equations

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

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

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

source
@[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.

Equations

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

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

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