Documentation

Mathlib.RingTheory.OreLocalization.Basic

Localization over right Ore sets. #

This file defines the localization of a monoid over a right Ore set and proves its universal mapping property. It then extends the definition and its properties first to semirings and then to rings. We show that in the case of a commutative monoid this definition coincides with the common monoid localization. Finally we show that in a ring without zero divisors, taking the Ore localization at R - {0} results in a division ring.

Notations #

Introduces the notation R[S⁻¹] for the Ore localization of a monoid R at a right Ore subset S. Also defines a new heterogeneous division notation r /ₒ s for a numerator r : R and a denominator s : S.

References #

Tags #

localization, Ore, non-commutative

The setoid on R × S used for the Ore localization.

Equations
Instances For
    def OreLocalization (R : Type u_1) [Monoid R] (S : Submonoid R) [OreLocalization.OreSet S] :
    Type u_1

    The ore localization of a monoid and a submonoid fulfilling the ore condition.

    Equations
    Instances For

      The ore localization of a monoid and a submonoid fulfilling the ore condition.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def OreLocalization.oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : S) :

        The division in the ore localization R[S⁻¹], as a fraction of an element of R and S.

        Equations
        Instances For

          The division in the ore localization R[S⁻¹], as a fraction of an element of R and S.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem OreLocalization.ind {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {β : OreLocalization R SProp} (c : ∀ (r : R) (s : S), β (r /ₒ s)) (q : OreLocalization R S) :
            β q
            theorem OreLocalization.oreDiv_eq_iff {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
            r₁ /ₒ s₁ = r₂ /ₒ s₂ ∃ (u : S) (v : R), r₂ * u = r₁ * v s₂ * u = s₁ * v
            theorem OreLocalization.expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : S) (t : R) (hst : s * t S) :
            r /ₒ s = r * t /ₒ { val := s * t, property := hst }

            A fraction r /ₒ s is equal to its expansion by an arbitrary factor t if s * t ∈ S.

            theorem OreLocalization.expand' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : S) (s' : S) :
            r /ₒ s = r * s' /ₒ (s * s')

            A fraction is equal to its expansion by a factor from s.

            theorem OreLocalization.eq_of_num_factor_eq {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {r' : R} {r₁ : R} {r₂ : R} {s : S} {t : S} (h : r * t = r' * t) :
            r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

            Fractions which differ by a factor of the numerator can be proven equal if those factors expand to equal elements of R.

            def OreLocalization.liftExpand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {C : Sort u_2} (P : RSC) (hP : ∀ (r t : R) (s : S) (ht : s * t S), P r s = P (r * t) { val := s * t, property := ht }) :
            OreLocalization R SC

            A function or predicate over R and S can be lifted to R[S⁻¹] if it is invariant under expansion on the right.

            Equations
            Instances For
              @[simp]
              theorem OreLocalization.liftExpand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {C : Sort u_2} {P : RSC} {hP : ∀ (r t : R) (s : S) (ht : s * t S), P r s = P (r * t) { val := s * t, property := ht }} (r : R) (s : S) :
              def OreLocalization.lift₂Expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {C : Sort u_2} (P : RSRSC) (hP : ∀ (r₁ t₁ : R) (s₁ : S) (ht₁ : s₁ * t₁ S) (r₂ t₂ : R) (s₂ : S) (ht₂ : s₂ * t₂ S), P r₁ s₁ r₂ s₂ = P (r₁ * t₁) { val := s₁ * t₁, property := ht₁ } (r₂ * t₂) { val := s₂ * t₂, property := ht₂ }) :

              A version of liftExpand used to simultaneously lift functions with two arguments in R[S⁻¹].

              Equations
              Instances For
                @[simp]
                theorem OreLocalization.lift₂Expand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {C : Sort u_2} {P : RSRSC} {hP : ∀ (r₁ t₁ : R) (s₁ : S) (ht₁ : s₁ * t₁ S) (r₂ t₂ : R) (s₂ : S) (ht₂ : s₂ * t₂ S), P r₁ s₁ r₂ s₂ = P (r₁ * t₁) { val := s₁ * t₁, property := ht₁ } (r₂ * t₂) { val := s₂ * t₂, property := ht₂ }} (r₁ : R) (s₁ : S) (r₂ : R) (s₂ : S) :
                OreLocalization.lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂

                The multiplication on the Ore localization of monoids.

                Equations
                Instances For
                  Equations
                  • OreLocalization.instMulOreLocalization = { mul := OreLocalization.mul }
                  theorem OreLocalization.oreDiv_mul_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
                  r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * OreLocalization.oreNum r₂ s₁ /ₒ (s₂ * OreLocalization.oreDenom r₂ s₁)
                  theorem OreLocalization.oreDiv_mul_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) (r' : R) (s' : S) (huv : r₂ * s' = s₁ * r') :
                  r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r' /ₒ (s₂ * s')

                  A characterization lemma for the multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.

                  def OreLocalization.oreDivMulChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) :
                  (r' : R) ×' (s' : S) ×' r₂ * s' = s₁ * r' r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r' /ₒ (s₂ * s')

                  Another characterization lemma for the multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.

                  Equations
                  Instances For
                    Equations
                    • OreLocalization.instOneOreLocalization = { one := 1 /ₒ 1 }
                    Equations
                    • OreLocalization.instInhabitedOreLocalization = { default := 1 }
                    @[simp]
                    theorem OreLocalization.div_eq_one' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} (hr : r S) :
                    r /ₒ { val := r, property := hr } = 1
                    @[simp]
                    theorem OreLocalization.div_eq_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {s : S} :
                    s /ₒ s = 1
                    theorem OreLocalization.one_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) :
                    1 * x = x
                    theorem OreLocalization.mul_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) :
                    x * 1 = x
                    theorem OreLocalization.mul_assoc {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) (y : OreLocalization R S) (z : OreLocalization R S) :
                    x * y * z = x * (y * z)
                    Equations
                    • OreLocalization.instMonoidOreLocalization = let __src := OreLocalization.instMulOreLocalization; let __src_1 := OreLocalization.instOneOreLocalization; Monoid.mk npowRec
                    theorem OreLocalization.mul_inv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (s : S) (s' : S) :
                    s /ₒ s' * (s' /ₒ s) = 1
                    @[simp]
                    theorem OreLocalization.mul_one_div {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {s : S} {t : S} :
                    r /ₒ s * (1 /ₒ t) = r /ₒ (t * s)
                    @[simp]
                    theorem OreLocalization.mul_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {s : S} {t : S} :
                    r /ₒ s * (s /ₒ t) = r /ₒ t
                    @[simp]
                    theorem OreLocalization.mul_cancel' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s : S} {t : S} :
                    r₁ /ₒ s * (s * r₂ /ₒ t) = r₁ * r₂ /ₒ t
                    @[simp]
                    theorem OreLocalization.div_one_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {p : R} {r : R} {s : S} :
                    r /ₒ 1 * (p /ₒ s) = r * p /ₒ s

                    The fraction s /ₒ 1 as a unit in R[S⁻¹], where s : S.

                    Equations
                    Instances For

                      The multiplicative homomorphism from R to R[S⁻¹], mapping r : R to the fraction r /ₒ 1.

                      Equations
                      • OreLocalization.numeratorHom = { toOneHom := { toFun := fun (r : R) => r /ₒ 1, map_one' := }, map_mul' := }
                      Instances For
                        theorem OreLocalization.numeratorHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} :
                        OreLocalization.numeratorHom r = r /ₒ 1
                        theorem OreLocalization.numerator_isUnit {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (s : S) :
                        IsUnit (OreLocalization.numeratorHom s)
                        def OreLocalization.universalMulHom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) :

                        The universal lift from a morphism R →* T, which maps elements of S to units of T, to a morphism R[S⁻¹] →* T.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem OreLocalization.universalMulHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) {r : R} {s : S} :
                          (OreLocalization.universalMulHom f fS hf) (r /ₒ s) = f r * (fS s)⁻¹
                          theorem OreLocalization.universalMulHom_commutes {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) {r : R} :
                          (OreLocalization.universalMulHom f fS hf) (OreLocalization.numeratorHom r) = f r
                          theorem OreLocalization.universalMulHom_unique {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) (φ : OreLocalization R S →* T) (huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) :

                          The universal morphism universalMulHom is unique.

                          theorem OreLocalization.oreDiv_mul_oreDiv_comm {R : Type u_1} [CommMonoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
                          r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
                          Equations
                          • OreLocalization.instCommMonoidOreLocalizationToMonoid = let __src := OreLocalization.instMonoidOreLocalization; CommMonoid.mk

                          The morphism numeratorHom is a monoid localization map in the case of commutative R.

                          Equations
                          • OreLocalization.localizationMap R S = { toMonoidHom := { toOneHom := { toFun := OreLocalization.numeratorHom, map_one' := }, map_mul' := }, map_units' := , surj' := , exists_of_eq := }
                          Instances For

                            If R is commutative, Ore localization and monoid localization are isomorphic.

                            Equations
                            Instances For
                              Equations
                              • OreLocalization.instAddOreLocalization = { add := OreLocalization.add }
                              theorem OreLocalization.oreDiv_add_oreDiv {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {r' : R} {s : S} {s' : S} :
                              r /ₒ s + r' /ₒ s' = (r * (OreLocalization.oreDenom (s) s') + r' * OreLocalization.oreNum (s) s') /ₒ (s * OreLocalization.oreDenom (s) s')
                              theorem OreLocalization.oreDiv_add_char {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {r' : R} (s : S) (s' : S) (rb : R) (sb : S) (h : s * sb = s' * rb) :
                              r /ₒ s + r' /ₒ s' = (r * sb + r' * rb) /ₒ (s * sb)

                              A characterization of the addition on the Ore localizaion, allowing for arbitrary Ore numerator and Ore denominator.

                              def OreLocalization.oreDivAddChar' {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (r' : R) (s : S) (s' : S) :
                              (r'' : R) ×' (s'' : S) ×' s * s'' = s' * r'' r /ₒ s + r' /ₒ s' = (r * s'' + r' * r'') /ₒ (s * s'')

                              Another characterization of the addition on the Ore localization, bundling up all witnesses and conditions into a sigma type.

                              Equations
                              Instances For
                                @[simp]
                                theorem OreLocalization.add_oreDiv {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {r' : R} {s : S} :
                                r /ₒ s + r' /ₒ s = (r + r') /ₒ s
                                theorem OreLocalization.add_assoc {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) (y : OreLocalization R S) (z : OreLocalization R S) :
                                x + y + z = x + (y + z)
                                Equations
                                • OreLocalization.instZeroOreLocalizationToMonoidToMonoidWithZero = { zero := OreLocalization.zero }
                                @[simp]
                                theorem OreLocalization.zero_div_eq_zero {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (s : S) :
                                0 /ₒ s = 0
                                theorem OreLocalization.add_comm {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) (y : OreLocalization R S) :
                                x + y = y + x
                                Equations
                                • OreLocalization.instAddCommMonoidOreLocalization = let __src := OreLocalization.instAddOreLocalization; AddCommMonoid.mk
                                theorem OreLocalization.left_distrib {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) (y : OreLocalization R S) (z : OreLocalization R S) :
                                x * (y + z) = x * y + x * z
                                theorem OreLocalization.right_distrib {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization R S) (y : OreLocalization R S) (z : OreLocalization R S) :
                                (x + y) * z = x * z + y * z
                                Equations
                                • One or more equations did not get rendered due to their size.
                                def OreLocalization.universalHom {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Semiring T] (f : R →+* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) :

                                The universal lift from a ring homomorphism f : R →+* T, which maps elements in S to units of T, to a ring homomorphism R[S⁻¹] →+* T. This extends the construction on monoids.

                                Equations
                                Instances For
                                  theorem OreLocalization.universalHom_apply {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Semiring T] (f : R →+* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) {r : R} {s : S} :
                                  (OreLocalization.universalHom f fS hf) (r /ₒ s) = f r * (fS s)⁻¹
                                  theorem OreLocalization.universalHom_commutes {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Semiring T] (f : R →+* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) {r : R} :
                                  (OreLocalization.universalHom f fS hf) (OreLocalization.numeratorHom r) = f r
                                  theorem OreLocalization.universalHom_unique {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Semiring T] (f : R →+* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) (φ : OreLocalization R S →+* T) (huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) :

                                  Negation on the Ore localization is defined via negation on the numerator.

                                  Equations
                                  Instances For
                                    Equations
                                    • OreLocalization.instNegOreLocalization = { neg := OreLocalization.neg }
                                    @[simp]
                                    theorem OreLocalization.neg_def {R : Type u_1} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] (r : R) (s : S) :
                                    -(r /ₒ s) = -r /ₒ s
                                    Equations
                                    • OreLocalization.ring = let __src := OreLocalization.instSemiringOreLocalization; let __src_1 := OreLocalization.instNegOreLocalization; Ring.mk zsmulRec
                                    theorem OreLocalization.numeratorHom_inj {R : Type u_1} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] (hS : S nonZeroDivisors R) :
                                    Function.Injective OreLocalization.numeratorHom

                                    The inversion of Ore fractions for a ring without zero divisors, satisying 0⁻¹ = 0 and (r /ₒ r')⁻¹ = r' /ₒ r for r ≠ 0.

                                    Equations
                                    Instances For
                                      Equations
                                      • OreLocalization.inv' = { inv := OreLocalization.inv }
                                      theorem OreLocalization.inv_def {R : Type u_1} [Ring R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] {r : R} {s : (nonZeroDivisors R)} :
                                      (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else s /ₒ { val := r, property := }
                                      Equations
                                      • One or more equations did not get rendered due to their size.