Mathlib.GroupTheory.OreLocalization.OreSet

AddOreLocalization.AddOreSet structure

{R : Type*} [AddMonoid R] (S : AddSubmonoid R)

Full source

/-- 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`. -/
class AddOreSet {R : Type*} [AddMonoid R] (S : AddSubmonoid R) where
  /-- Common summands on the right can be turned into common summands on the left, a weak form of
cancellability. -/
  ore_right_cancel : ∀ (r₁ r₂ : R) (s : S), r₁ + s = r₂ + s → ∃ s' : S, s' + r₁ = s' + r₂
  /-- The Ore minuend of a difference. -/
  oreMin : R → S → R
  /-- The Ore subtrahend of a difference. -/
  oreSubtra : R → S → S
  /-- The Ore condition of a difference, expressed in terms of `oreMin` and `oreSubtra`. -/
  ore_eq : ∀ (r : R) (s : S), oreSubtra r s + r = oreMin r s + s

Left Ore set in an additive monoid

Informal description

A subset $S$ of an additive monoid $R$ is called a *left Ore set* if it satisfies the following conditions: 1. $S$ is an additive submonoid of $R$ (i.e., it contains $0$ and is closed under addition). 2. For any $r \in R$ and $s \in S$, there exist $v \in R$ and $u \in S$ such that $u + r = v + s$. 3. For any $r_1, r_2 \in R$ and $s \in S$, if $r_1 + s = r_2 + s$, then there exists $s' \in S$ such that $s' + r_1 = s' + r_2$.

OreLocalization.OreSet structure

{R : Type*} [Monoid R] (S : Submonoid R)

Full source

/-- 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`. -/
@[to_additive AddOreLocalization.AddOreSet]
class OreSet {R : Type*} [Monoid R] (S : Submonoid R) where
  /-- Common factors on the right can be turned into common factors on the left, a weak form of
cancellability. -/
  ore_right_cancel : ∀ (r₁ r₂ : R) (s : S), r₁ * s = r₂ * s → ∃ s' : S, s' * r₁ = s' * r₂
  /-- The Ore numerator of a fraction. -/
  oreNum : R → S → R
  /-- The Ore denominator of a fraction. -/
  oreDenom : R → S → S
  /-- The Ore condition of a fraction, expressed in terms of `oreNum` and `oreDenom`. -/
  ore_eq : ∀ (r : R) (s : S), oreDenom r s * r = oreNum r s * s

Left Ore set in a monoid

Informal description

A submonoid $S$ of a monoid $R$ is called a *left Ore set* if it satisfies the following conditions: 1. For any $r \in R$ and $s \in S$, there exist $v \in R$ and $u \in S$ such that $u \cdot r = v \cdot s$. 2. For any $r_1, r_2 \in R$ and $s \in S$, if $r_1 \cdot s = r_2 \cdot s$, then there exists $s' \in S$ such that $s' \cdot r_1 = s' \cdot r_2$.

OreLocalization.ore_right_cancel theorem

(r₁ r₂ : R) (s : S) (h : r₁ * s = r₂ * s) : ∃ s' : S, s' * r₁ = s' * r₂

Full source

/-- Common factors on the right can be turned into common factors on the left, a weak form of
cancellability. -/
@[to_additive AddOreLocalization.ore_right_cancel]
theorem ore_right_cancel (r₁ r₂ : R) (s : S) (h : r₁ * s = r₂ * s) : ∃ s' : S, s' * r₁ = s' * r₂ :=
  OreSet.ore_right_cancel r₁ r₂ s h

Right Cancellation Property for Left Ore Sets

Informal description

Let $R$ be a monoid and $S$ a left Ore set in $R$. For any elements $r_1, r_2 \in R$ and $s \in S$ such that $r_1 \cdot s = r_2 \cdot s$, there exists an element $s' \in S$ such that $s' \cdot r_1 = s' \cdot r_2$.

OreLocalization.oreNum definition

(r : R) (s : S) : R

Full source

/-- The Ore numerator of a fraction. -/
@[to_additive AddOreLocalization.oreMin "The Ore minuend of a difference."]
def oreNum (r : R) (s : S) : R :=
  OreSet.oreNum r s

Ore numerator of a fraction

Informal description

Given a monoid $R$ with a left Ore set $S \subseteq R$, the function $\text{oreNum}$ takes an element $r \in R$ and $s \in S$ and returns an element $v \in R$ such that there exists $u \in S$ satisfying $u \cdot r = v \cdot s$. This element $v$ is called the *Ore numerator* of the fraction $r/s$.

OreLocalization.oreDenom definition

(r : R) (s : S) : S

Full source

/-- The Ore denominator of a fraction. -/
@[to_additive AddOreLocalization.oreSubtra "The Ore subtrahend of a difference."]
def oreDenom (r : R) (s : S) : S :=
  OreSet.oreDenom r s

Ore denominator of a fraction

Informal description

For a given element $r$ in a monoid $R$ and an element $s$ in a left Ore set $S$ of $R$, the function `oreDenom` returns an element $s' \in S$ such that there exists $r' \in R$ satisfying $s' \cdot r = r' \cdot s$.

OreLocalization.ore_eq theorem

(r : R) (s : S) : oreDenom r s * r = oreNum r s * s

Full source

/-- The Ore condition of a fraction, expressed in terms of `oreNum` and `oreDenom`. -/
@[to_additive AddOreLocalization.add_ore_eq
  "The Ore condition of a difference, expressed in terms of `oreMin` and `oreSubtra`."]
theorem ore_eq (r : R) (s : S) : oreDenom r s * r = oreNum r s * s :=
  OreSet.ore_eq r s

Ore Condition for Fraction Representation

Informal description

For any element $r$ in a monoid $R$ and any element $s$ in a left Ore set $S \subseteq R$, the Ore condition holds: \[ \text{oreDenom}(r, s) \cdot r = \text{oreNum}(r, s) \cdot s \] where $\text{oreDenom}(r, s) \in S$ and $\text{oreNum}(r, s) \in R$ are the Ore denominator and numerator respectively.

OreLocalization.oreCondition definition

(r : R) (s : S) : Σ' r' : R, Σ' s' : S, s' * r = r' * s

Full source

/-- 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. -/
@[to_additive AddOreLocalization.addOreCondition
  "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."]
def oreCondition (r : R) (s : S) : Σ'r' : R, Σ's' : S, s' * r = r' * s :=
  ⟨oreNum r s, oreDenom r s, ore_eq r s⟩

Ore condition for left Ore sets

Informal description

For any element $ r $ in a monoid $ R $ and any element $ s $ in a left Ore set $ S \subseteq R $, there exist elements $ r' \in R $ and $ s' \in S $ such that $ s' \cdot r = r' \cdot s $. This condition ensures the existence of a common denominator for fractions in the Ore localization.

OreLocalization.oreSetBot instance

: OreSet (⊥ : Submonoid R)

Full source

/-- The trivial submonoid is an Ore set. -/
@[to_additive AddOreLocalization.addOreSetBot]
instance oreSetBot : OreSet (⊥ : Submonoid R) where
  ore_right_cancel _ _ s h :=
    ⟨s, by
      rcases s with ⟨s, hs⟩
      rw [Submonoid.mem_bot] at hs
      subst hs
      rw [mul_one, mul_one] at h
      subst h
      rfl⟩
  oreNum r _ := r
  oreDenom _ s := s
  ore_eq _ s := by
    rcases s with ⟨s, hs⟩
    rw [Submonoid.mem_bot] at hs
    simp [hs]

Trivial Submonoid as Left Ore Set

Informal description

The trivial submonoid $\{1\}$ of a monoid $R$ is a left Ore set.

OreLocalization.oreSetComm instance

{R} [CommMonoid R] (S : Submonoid R) : OreSet S

Full source

/-- Every submonoid of a commutative monoid is an Ore set. -/
@[to_additive AddOreLocalization.addOreSetComm]
instance (priority := 100) oreSetComm {R} [CommMonoid R] (S : Submonoid R) : OreSet S where
  ore_right_cancel m n s h := ⟨s, by rw [mul_comm (s : R) n, mul_comm (s : R) m, h]⟩
  oreNum r _ := r
  oreDenom _ s := s
  ore_eq r s := by rw [mul_comm]

Submonoids in Commutative Monoids are Ore Sets

Informal description

For any commutative monoid $R$ and submonoid $S$ of $R$, $S$ is a left Ore set in $R$.

References