Documentation

Mathlib.GroupTheory.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) :

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

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

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

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

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

                  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 := }
                  Equations
                  • AddOreLocalization.addOreSetBot = { ore_right_cancel := , oreMin := fun (r : R) (x : ) => r, oreSubtra := fun (x : R) (s : ) => s, ore_eq := }
                  @[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 := }
                  @[instance 100]
                  Equations