Documentation

Mathlib.RingTheory.OreLocalization.OreSet

(Right) Ore sets #

This defines right Ore sets on arbitrary monoids.

References #

class OreLocalization.OreSet {R : Type u_1} [inst : Monoid R] (S : Submonoid R) :
Type u_1
  • Common factors on the left can be turned into common factors on the right, a weak form of cancellability.

    ore_left_cancel : ∀ (r₁ r₂ : R) (s : { x // x S }), s * r₁ = s * r₂s', r₁ * s' = r₂ * s'
  • The Ore numerator of a fraction.

    oreNum : R{ x // x S }R
  • The Ore denominator of a fraction.

    oreDenom : R{ x // x S }{ x // x S }
  • The Ore condition of a fraction, expressed in terms of oreNum and oreDenom.

    ore_eq : ∀ (r : R) (s : { x // x S }), r * ↑(oreDenom r s) = s * oreNum r s

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
    theorem OreLocalization.ore_left_cancel {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst : OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s : { x // x S }) (h : s * r₁ = s * r₂) :
    s', r₁ * s' = r₂ * s'

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

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

    The Ore numerator of a fraction.

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

    The Ore denominator of a fraction.

    Equations
    theorem OreLocalization.ore_eq {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst : OreLocalization.OreSet S] (r : R) (s : { x // x S }) :

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

    def OreLocalization.oreCondition {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst : OreLocalization.OreSet S] (r : R) (s : { x // x S }) :
    (r' : R) ×' (s' : { x // x 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
    • One or more equations did not get rendered due to their size.

    The trivial submonoid is an Ore set.

    Equations
    • One or more equations did not get rendered due to their size.

    Every submonoid of a commutative monoid is an Ore set.

    Equations
    • One or more equations did not get rendered due to their size.
    def OreLocalization.oreSetOfCancelMonoidWithZero {R : Type u_1} [inst : CancelMonoidWithZero R] {S : Submonoid R} (oreNum : R{ x // x S }R) (oreDenom : R{ x // x S }{ x // x S }) (ore_eq : ∀ (r : R) (s : { x // x S }), r * ↑(oreDenom r s) = s * oreNum r s) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    def OreLocalization.oreSetOfNoZeroDivisors {R : Type u_1} [inst : Ring R] [inst : NoZeroDivisors R] {S : Submonoid R} (oreNum : R{ x // x S }R) (oreDenom : R{ x // x S }{ x // x S }) (ore_eq : ∀ (r : R) (s : { x // x S }), r * ↑(oreDenom r s) = s * oreNum r 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