mathlib3 documentation

ring_theory.ore_localization.ore_set

(Right) Ore sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines right Ore sets on arbitrary monoids.

References #

source
@[class]
structure ore_localization.ore_set {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.

Instances of this typeclass
Instances of other typeclasses for ore_localization.ore_set
  • ore_localization.ore_set.has_sizeof_inst
source
theorem ore_localization.ore_left_cancel {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (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.

source
def ore_localization.ore_num {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s : ↥S) :
R

The Ore numerator of a fraction.

Equations
source
def ore_localization.ore_denom {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s : ↥S) :
↥S

The Ore denominator of a fraction.

Equations
source
theorem ore_localization.ore_eq {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set S] (r : R) (s : ↥S) :
r * ↑(ore_localization.ore_denom r s) = ↑s * ore_localization.ore_num r s

The Ore condition of a fraction, expressed in terms of ore_num and ore_denom.

source
def ore_localization.ore_condition {R : Type u_1} [monoid R] {S : submonoid R} [ore_localization.ore_set 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
source
@[protected, instance]
def ore_localization.ore_set_bot {R : Type u_1} [monoid R] :
ore_localization.ore_set ⊥

The trivial submonoid is an Ore set.

Equations
source
@[protected, instance]
def ore_localization.ore_set_comm {R : Type u_1} [comm_monoid R] (S : submonoid R) :
ore_localization.ore_set S

Every submonoid of a commutative monoid is an Ore set.

Equations
source
def ore_localization.ore_set_of_cancel_monoid_with_zero {R : Type u_1} [cancel_monoid_with_zero R] {S : submonoid R} (ore_num : R → ↥S → R) (ore_denom : R → ↥S → ↥S) (ore_eq : ∀ (r : R) (s : ↥S), r * ↑(ore_denom r s) = ↑s * ore_num r s) :
ore_localization.ore_set S

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

Equations
source
def ore_localization.ore_set_of_no_zero_divisors {R : Type u_1} [ring R] [no_zero_divisors R] {S : submonoid R} (ore_num : R → ↥S → R) (ore_denom : R → ↥S → ↥S) (ore_eq : ∀ (r : R) (s : ↥S), r * ↑(ore_denom r s) = ↑s * ore_num r s) :
ore_localization.ore_set 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