Documentation

Mathlib.RingTheory.OreLocalization.OreSet

(Left) Ore sets #

This defines left Ore sets on arbitrary monoids.

References #

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 : RSR

    The Ore minuend of a difference.

  • oreSubtra : RSS

    The Ore subtrahend of a difference.

  • ore_eq : ∀ (r : R) (s : S), (AddOreLocalization.AddOreSet.oreSubtra r s) + r = AddOreLocalization.AddOreSet.oreMin r s + s

    The Ore condition of a difference, expressed in terms of oreMin and oreSubtra.

Instances
    theorem AddOreLocalization.AddOreSet.ore_right_cancel {R : Type u_1} :
    ∀ {inst : AddMonoid R} {S : AddSubmonoid R} [self : AddOreLocalization.AddOreSet S] (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.

    The Ore condition of a difference, expressed in terms of oreMin and oreSubtra.

    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 : RSR

      The Ore numerator of a fraction.

    • oreDenom : RSS

      The Ore denominator of a fraction.

    • ore_eq : ∀ (r : R) (s : S), (OreLocalization.OreSet.oreDenom r s) * r = OreLocalization.OreSet.oreNum r s * s

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

    Instances
      theorem OreLocalization.OreSet.ore_right_cancel {R : Type u_1} :
      ∀ {inst : Monoid R} {S : Submonoid R} [self : OreLocalization.OreSet S] (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.

      theorem OreLocalization.OreSet.ore_eq {R : Type u_1} :
      ∀ {inst : Monoid R} {S : Submonoid R} [self : OreLocalization.OreSet S] (r : R) (s : S), (OreLocalization.OreSet.oreDenom r s) * r = OreLocalization.OreSet.oreNum r s * s

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

      theorem AddOreLocalization.ore_right_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s : S) (h : r₁ + s = r₂ + s) :
      ∃ (s' : S), s' + r₁ = s' + r₂
      theorem OreLocalization.ore_right_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ : 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.

      def AddOreLocalization.oreMin {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r : R) (s : S) :
      R

      The Ore minuend of a difference.

      Equations
      Instances For
        def OreLocalization.oreNum {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : S) :
        R

        The Ore numerator of a fraction.

        Equations
        Instances For
          def AddOreLocalization.oreSubtra {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r : R) (s : S) :
          S

          The Ore subtrahend of a difference.

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

            The Ore denominator of a fraction.

            Equations
            Instances For

              The Ore condition of a difference, expressed in terms of oreMin and oreSubtra.

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

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

              def AddOreLocalization.addOreCondition {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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
              Instances For
                def OreLocalization.oreCondition {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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
                Instances For
                  Equations
                  • AddOreLocalization.addOreSetBot = { ore_right_cancel := , oreMin := fun (r : R) (x : ) => r, oreSubtra := fun (x : R) (s : ) => s, ore_eq := }
                  theorem AddOreLocalization.addOreSetBot.proof_1 {R : Type u_1} [AddMonoid R] :
                  ∀ (x x_1 : R) (s : ), x + s = x_1 + s∃ (s' : ), s' + x = s' + x_1
                  theorem AddOreLocalization.addOreSetBot.proof_2 {R : Type u_1} [AddMonoid R] :
                  ∀ (x : R) (s : ), ((fun (x : R) (s : ) => s) x s) + x = (fun (r : R) (x : ) => r) x s + s

                  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 := }
                  theorem AddOreLocalization.addOreSetComm.proof_1 {R : Type u_1} [AddCommMonoid R] (S : AddSubmonoid R) (m : R) (n : R) (s : S) (h : m + s = n + s) :
                  ∃ (s' : S), s' + m = s' + n
                  theorem AddOreLocalization.addOreSetComm.proof_2 {R : Type u_1} [AddCommMonoid R] (S : AddSubmonoid R) (r : R) (s : S) :
                  ((fun (x : R) (s : S) => s) r s) + r = (fun (r : R) (x : S) => r) r s + s
                  @[instance 100]
                  Equations
                  @[instance 100]

                  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 := }
                  def OreLocalization.oreSetOfCancelMonoidWithZero {R : Type u_1} [CancelMonoidWithZero R] {S : Submonoid R} (oreNum : RSR) (oreDenom : RSS) (ore_eq : ∀ (r : R) (s : S), (oreDenom r s) * r = oreNum r s * s) :

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

                  Equations
                  Instances For
                    def OreLocalization.oreSetOfNoZeroDivisors {R : Type u_1} [Ring R] [NoZeroDivisors R] {S : Submonoid R} (oreNum : RSR) (oreDenom : RSS) (ore_eq : ∀ (r : R) (s : S), (oreDenom r s) * r = oreNum r s * 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
                    Instances For
                      theorem OreLocalization.nonempty_oreSet_iff {R : Type u_1} [Ring R] {S : Submonoid R} :
                      Nonempty (OreLocalization.OreSet S) (∀ (r₁ r₂ : R) (s : S), r₁ * s = r₂ * s∃ (s' : S), s' * r₁ = s' * r₂) ∀ (r : R) (s : S), ∃ (r' : R) (s' : S), s' * r = r' * s
                      theorem OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors {R : Type u_1} [Ring R] [NoZeroDivisors R] {S : Submonoid R} :
                      Nonempty (OreLocalization.OreSet S) ∀ (r : R) (s : S), ∃ (r' : R) (s' : S), s' * r = r' * s