Documentation

Mathlib.RingTheory.OreLocalization.OreSet

(Right) Ore sets #

This defines right Ore sets on arbitrary monoids.

References #

source
class OreLocalization.OreSet {R : Type u_1} [Monoid R] (S : Submonoid R) :
Type u_1
  • ore_left_cancel : ∀ (r₁ r₂ : R) (s : { x // x ∈ S }), ↑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.

  • oreNum : R → { x // x ∈ S } → R

    The Ore numerator of a fraction.

  • oreDenom : R → { x // x ∈ S } → { x // x ∈ S }

    The Ore denominator of a fraction.

  • ore_eq : ∀ (r : R) (s_1 : { x // x ∈ S }), r * ↑(OreLocalization.OreSet.oreDenom r s_1) = ↑s_1 * OreLocalization.OreSet.oreNum r s_1

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

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
    source
    theorem OreLocalization.ore_left_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [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.

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

    The Ore numerator of a fraction.

    Instances For
      source
      def OreLocalization.oreDenom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : { x // x ∈ S }) :
      { x // x ∈ S }

      The Ore denominator of a fraction.

      Instances For
        source
        theorem OreLocalization.ore_eq {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : { x // x ∈ S }) :
        r * ↑(OreLocalization.oreDenom r s) = ↑s * OreLocalization.oreNum r s

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

        source
        def OreLocalization.oreCondition {R : Type u_1} [Monoid R] {S : Submonoid R} [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.

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

          The trivial submonoid is an Ore set.

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

          Every submonoid of a commutative monoid is an Ore set.

          source
          def OreLocalization.oreSetOfCancelMonoidWithZero {R : Type u_1} [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) :
          OreLocalization.OreSet S

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

          Instances For
            source
            def OreLocalization.oreSetOfNoZeroDivisors {R : Type u_1} [Ring R] [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) :
            OreLocalization.OreSet S

            In rings without zero divisors, the first (cancellability) condition is always fulfilled, it suffices to give a proof for the Ore condition itself.

            Instances For