Localization over left Ore sets.

This file defines the localization of a monoid over a left Ore set and proves its universal mapping property.

Notation

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

• https://ncatlab.org/nlab/show/Ore+localization
• [Zoran Škoda, Noncommutative localization in noncommutative geometry][skoda2006]

Tags

localization, Ore, non-commutative

Implementation detail

Some of the declarations are marked reducible to avoid diamonds with Mathlib/Algebra/Module/LocalizedModule/Basic.lean. This causes a significant performance regression, most notabaly in Mathlib/AlgebraicGeometry/AffineSpace.lean. Also see https://github.com/leanprover-community/mathlib4/pull/31862.

We shall investigate if there are ways to improve performances. For example by introducing typeclasses to unify the two constructions on this and LocalizedModule, or by marking some downstream constructions (e.g. Spec.structureSheaf) as irreducible.

def OreLocalization.oreEqv {R : Type u_1} [Monoid R] (S : Submonoid R) [OreSet S] (X : Type u_2) [MulAction R X] : Setoid (X × ↥S)

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

Equations

• OreLocalization.oreEqv S X = { r := fun (rs rs' : X × ↥S) => ∃ (u : ↥S) (v : R), u • rs'.1 = v • rs.1 ∧ ↑u * ↑rs'.2 = v * ↑rs.2, iseqv := ⋯ }

def AddOreLocalization.oreEqv {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) [AddOreSet S] (X : Type u_2) [AddAction R X] : Setoid (X × ↥S)

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

Equations

• AddOreLocalization.oreEqv S X = { r := fun (rs rs' : X × ↥S) => ∃ (u : ↥S) (v : R), u +ᵥ rs'.1 = v +ᵥ rs.1 ∧ ↑u + ↑rs'.2 = v + ↑rs.2, iseqv := ⋯ }

def OreLocalization {R : Type u_1} [Monoid R] (S : Submonoid R) [OreLocalization.OreSet S] (X : Type u_2) [MulAction R X] : Type (max u_1 u_2)

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

Equations

• OreLocalization S X = Quotient (OreLocalization.oreEqv S X)

def AddOreLocalization {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) [AddOreLocalization.AddOreSet S] (X : Type u_2) [AddAction R X] : Type (max u_1 u_2)

The Ore localization of an additive monoid and a submonoid fulfilling the Ore condition.

Equations

• AddOreLocalization S X = Quotient (AddOreLocalization.oreEqv S X)

def OreLocalization.«term__[_⁻¹_]» : Lean.TrailingParserDescr

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.

def OreLocalization.oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (r : X) (s : ↥S) : OreLocalization S X

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

Equations

• r /ₒ s = Quotient.mk' (r, s)

def AddOreLocalization.oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s : ↥S) : AddOreLocalization S X

The subtraction in the Ore localization, as a difference of an element of X and S.

Equations

• r -ₒ s = Quotient.mk' (r, s)

def OreLocalization.«term_/ₒ_» : Lean.TrailingParserDescr

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

Equations

• OreLocalization.«term_/ₒ_» = Lean.ParserDescr.trailingNode `OreLocalization.«term_/ₒ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ₒ ") (Lean.ParserDescr.cat `term 71))

def OreLocalization.«term_-ₒ_» : Lean.TrailingParserDescr

The subtraction in the Ore localization, as a difference of an element of X and S.

Equations

• OreLocalization.«term_-ₒ_» = Lean.ParserDescr.trailingNode `OreLocalization.«term_-ₒ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -ₒ ") (Lean.ParserDescr.cat `term 66))

theorem OreLocalization.ind {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {β : OreLocalization S X → Prop} (c : ∀ (r : X) (s : ↥S), β (r /ₒ s)) (q : OreLocalization S X) : β q

theorem AddOreLocalization.ind {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {β : AddOreLocalization S X → Prop} (c : ∀ (r : X) (s : ↥S), β (r -ₒ s)) (q : AddOreLocalization S X) : β q

theorem OreLocalization.oreDiv_eq_iff {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {r₁ r₂ : X} {s₁ s₂ : ↥S} : r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ (u : ↥S) (v : R), u • r₂ = v • r₁ ∧ ↑u * ↑s₂ = v * ↑s₁

theorem AddOreLocalization.oreSub_eq_iff {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ r₂ : X} {s₁ s₂ : ↥S} : r₁ -ₒ s₁ = r₂ -ₒ s₂ ↔ ∃ (u : ↥S) (v : R), u +ᵥ r₂ = v +ᵥ r₁ ∧ ↑u + ↑s₂ = v + ↑s₁

theorem OreLocalization.expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (r : X) (s : ↥S) (t : R) (hst : t * ↑s ∈ S) : r /ₒ s = t • r /ₒ ⟨t * ↑s, hst⟩

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

theorem AddOreLocalization.expand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s : ↥S) (t : R) (hst : t + ↑s ∈ S) : r -ₒ s = (t +ᵥ r) -ₒ ⟨t + ↑s, hst⟩

A difference r -ₒ s is equal to its expansion by an arbitrary translation t if t + s ∈ S.

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

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

theorem AddOreLocalization.expand' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s s' : ↥S) : r -ₒ s = (s' +ᵥ r) -ₒ (s' + s)

A difference is equal to its expansion by a summand from S.

theorem OreLocalization.eq_of_num_factor_eq {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r r' r₁ r₂ : R} {s t : ↥S} (h : ↑t * r = ↑t * r') : 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.

theorem AddOreLocalization.eq_of_num_factor_eq {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r r' r₁ r₂ : R} {s t : ↥S} (h : ↑t + r = ↑t + r') : r₁ + r + r₂ -ₒ s = r₁ + r' + r₂ -ₒ s

Differences whose minuends differ by a common summand can be proven equal if those summands expand to equal elements of R.

def OreLocalization.liftExpand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} (P : X → ↥S → C) (hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩) : OreLocalization S X → C

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

Equations

• OreLocalization.liftExpand P hP = Quotient.lift (fun (p : X × ↥S) => P p.1 p.2) ⋯

def AddOreLocalization.liftExpand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} (P : X → ↥S → C) (hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩) : AddOreLocalization S X → C

A function or predicate over X and S can be lifted to the localization if it is invariant under expansion on the left.

Equations

• AddOreLocalization.liftExpand P hP = Quotient.lift (fun (p : X × ↥S) => P p.1 p.2) ⋯

@[simp]

theorem OreLocalization.liftExpand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} {P : X → ↥S → C} {hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩} (r : X) (s : ↥S) : liftExpand P hP (r /ₒ s) = P r s

@[simp]

theorem AddOreLocalization.liftExpand_of {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} {P : X → ↥S → C} {hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩} (r : X) (s : ↥S) : liftExpand P hP (r -ₒ s) = P r s

def OreLocalization.lift₂Expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} (P : X → ↥S → X → ↥S → C) (hP : ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S), P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩) : OreLocalization S X → OreLocalization S X → C

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

Equations

• OreLocalization.lift₂Expand P hP = OreLocalization.liftExpand (fun (r₁ : X) (s₁ : ↥S) => OreLocalization.liftExpand (P r₁ s₁) ⋯) ⋯

def AddOreLocalization.lift₂Expand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} (P : X → ↥S → X → ↥S → C) (hP : ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S), P r₁ s₁ r₂ s₂ = P (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩) : AddOreLocalization S X → AddOreLocalization S X → C

A version of liftExpand used to simultaneously lift functions with two arguments.

Equations

• AddOreLocalization.lift₂Expand P hP = AddOreLocalization.liftExpand (fun (r₁ : X) (s₁ : ↥S) => AddOreLocalization.liftExpand (P r₁ s₁) ⋯) ⋯

@[simp]

theorem OreLocalization.lift₂Expand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} {P : X → ↥S → X → ↥S → C} {hP : ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S), P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩} (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S) : lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂

@[simp]

theorem AddOreLocalization.lift₂Expand_of {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} {P : X → ↥S → X → ↥S → C} {hP : ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S), P r₁ s₁ r₂ s₂ = P (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩} (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S) : lift₂Expand P hP (r₁ -ₒ s₁) (r₂ -ₒ s₂) = P r₁ s₁ r₂ s₂

@[reducible, inline]

abbrev OreLocalization.smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (y : OreLocalization S R) (x : OreLocalization S X) : OreLocalization S X

The scalar multiplication on the Ore localization of monoids.

Equations

• y.smul x = OreLocalization.liftExpand (fun (x1 : R) (x2 : ↥S) => OreLocalization.smul''✝ x1 x2 x) ⋯ y

@[reducible, inline]

abbrev AddOreLocalization.vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (y : AddOreLocalization S R) (x : AddOreLocalization S X) : AddOreLocalization S X

the vector addition on the Ore localization of additive monoids.

Equations

• y.vadd x = AddOreLocalization.liftExpand (fun (x1 : R) (x2 : ↥S) => AddOreLocalization.vadd''✝ x1 x2 x) ⋯ y

instance OreLocalization.instSMul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] : SMul (OreLocalization S R) (OreLocalization S X)

Equations

• OreLocalization.instSMul = { smul := OreLocalization.smul }

instance AddOreLocalization.instVAdd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] : VAdd (AddOreLocalization S R) (AddOreLocalization S X)

Equations

• AddOreLocalization.instVAdd = { vadd := AddOreLocalization.vadd }

instance OreLocalization.instMul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] : Mul (OreLocalization S R)

Equations

• OreLocalization.instMul = { mul := OreLocalization.smul }

instance AddOreLocalization.instAdd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] : Add (AddOreLocalization S R)

Equations

• AddOreLocalization.instAdd = { add := AddOreLocalization.vadd }

theorem OreLocalization.oreDiv_smul_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {r₁ : R} {r₂ : X} {s₁ s₂ : ↥S} : (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

theorem AddOreLocalization.oreSub_vadd_oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ : R} {r₂ : X} {s₁ s₂ : ↥S} : (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (oreMin r₁ s₂ +ᵥ r₂) -ₒ (oreSubtra r₁ s₂ + s₁)

theorem OreLocalization.oreDiv_mul_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S} : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

theorem AddOreLocalization.oreSub_add_oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S} : r₁ -ₒ s₁ + (r₂ -ₒ s₂) = oreMin r₁ s₂ + r₂ -ₒ (oreSubtra r₁ s₂ + s₁)

theorem OreLocalization.oreDiv_smul_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S) (huv : ↑s' * r₁ = r' * ↑s₂) : (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

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

theorem AddOreLocalization.oreSub_vadd_char {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S) (huv : ↑s' + r₁ = r' + ↑s₂) : (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (r' +ᵥ r₂) -ₒ (s' + s₁)

A characterization lemma for the vector addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.

theorem OreLocalization.oreDiv_mul_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (r₁ r₂ : R) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S) (huv : ↑s' * r₁ = r' * ↑s₂) : 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.

theorem AddOreLocalization.oreSub_add_char {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (r₁ r₂ : R) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S) (huv : ↑s' + r₁ = r' + ↑s₂) : r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)

A characterization lemma for the addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.

def OreLocalization.oreDivSMulChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) : (r' : R) ×' (s' : ↥S) ×' ↑s' * r₁ = r' * ↑s₂ ∧ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

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

Equations

• OreLocalization.oreDivSMulChar' r₁ r₂ s₁ s₂ = ⟨OreLocalization.oreNum r₁ s₂, ⟨OreLocalization.oreDenom r₁ s₂, ⋯⟩⟩

def AddOreLocalization.oreSubVAddChar' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) : (r' : R) ×' (s' : ↥S) ×' ↑s' + r₁ = r' + ↑s₂ ∧ (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (r' +ᵥ r₂) -ₒ (s' + s₁)

Another characterization lemma for the vector addition on the Ore localization delivering Ore witnesses and conditions bundled in a sigma type.

Equations

• AddOreLocalization.oreSubVAddChar' r₁ r₂ s₁ s₂ = ⟨AddOreLocalization.oreMin r₁ s₂, ⟨AddOreLocalization.oreSubtra r₁ s₂, ⋯⟩⟩

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

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

Equations

• OreLocalization.oreDivMulChar' r₁ r₂ s₁ s₂ = ⟨OreLocalization.oreNum r₁ s₂, ⟨OreLocalization.oreDenom r₁ s₂, ⋯⟩⟩

def AddOreLocalization.oreSubAddChar' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (r₁ r₂ : R) (s₁ s₂ : ↥S) : (r' : R) ×' (s' : ↥S) ×' ↑s' + r₁ = r' + ↑s₂ ∧ r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)

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

Equations

• AddOreLocalization.oreSubAddChar' r₁ r₂ s₁ s₂ = ⟨AddOreLocalization.oreMin r₁ s₂, ⟨AddOreLocalization.oreSubtra r₁ s₂, ⋯⟩⟩

@[irreducible]

def OreLocalization.one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] [One X] : OreLocalization S X

1 in the localization, defined as 1 /ₒ 1.

Equations

• OreLocalization.one = 1 /ₒ 1

@[irreducible]

def AddOreLocalization.zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] [Zero X] : AddOreLocalization S X

0 in the additive localization, defined as 0 -ₒ 0.

Equations

• AddOreLocalization.zero = 0 -ₒ 0

instance OreLocalization.instOne {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] [One X] : One (OreLocalization S X)

Equations

• OreLocalization.instOne = { one := OreLocalization.one }

instance AddOreLocalization.instZero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] [Zero X] : Zero (AddOreLocalization S X)

Equations

• AddOreLocalization.instZero = { zero := AddOreLocalization.zero }

theorem OreLocalization.one_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] [One X] : 1 = 1 /ₒ 1

theorem AddOreLocalization.zero_def {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] [Zero X] : 0 = 0 -ₒ 0

instance OreLocalization.instInhabited {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] : Inhabited (OreLocalization S R)

Equations

• OreLocalization.instInhabited = { default := 1 }

instance AddOreLocalization.instInhabited {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] : Inhabited (AddOreLocalization S R)

Equations

• AddOreLocalization.instInhabited = { default := 0 }

@[simp]

theorem OreLocalization.div_eq_one' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r : R} (hr : r ∈ S) : r /ₒ ⟨r, hr⟩ = 1

@[simp]

theorem AddOreLocalization.sub_eq_zero' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r : R} (hr : r ∈ S) : r -ₒ ⟨r, hr⟩ = 0

@[simp]

theorem OreLocalization.div_eq_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {s : ↥S} : ↑s /ₒ s = 1

@[simp]

theorem AddOreLocalization.sub_eq_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {s : ↥S} : ↑s -ₒ s = 0

theorem OreLocalization.one_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (x : OreLocalization S X) : 1 • x = x

theorem AddOreLocalization.zero_vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (x : AddOreLocalization S X) : 0 +ᵥ x = x

theorem OreLocalization.one_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (x : OreLocalization S R) : 1 * x = x

theorem AddOreLocalization.zero_add {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (x : AddOreLocalization S R) : 0 + x = x

theorem OreLocalization.mul_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (x : OreLocalization S R) : x * 1 = x

theorem AddOreLocalization.add_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (x : AddOreLocalization S R) : x + 0 = x

theorem OreLocalization.mul_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] (x y : OreLocalization S R) (z : OreLocalization S X) : (x * y) • z = x • y • z

theorem AddOreLocalization.add_vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] (x y : AddOreLocalization S R) (z : AddOreLocalization S X) : (x + y) +ᵥ z = x +ᵥ y +ᵥ z

theorem OreLocalization.mul_assoc {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (x y z : OreLocalization S R) : x * y * z = x * (y * z)

theorem AddOreLocalization.add_assoc {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (x y z : AddOreLocalization S R) : x + y + z = x + (y + z)

@[reducible, inline]

abbrev OreLocalization.npow {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] : ℕ → OreLocalization S R → OreLocalization S R

npow of OreLocalization

Equations

• OreLocalization.npow = npowRec

@[reducible, inline]

abbrev AddOreLocalization.nsmul {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] : ℕ → AddOreLocalization S R → AddOreLocalization S R

nsmul of AddOreLocalization

Equations

• AddOreLocalization.nsmul = nsmulRec

instance OreLocalization.instMonoid {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] : Monoid (OreLocalization S R)

Equations

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

instance AddOreLocalization.instAddMonoid {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] : AddMonoid (AddOreLocalization S R)

Equations

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

instance OreLocalization.instMulActionOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] : MulAction (OreLocalization S R) (OreLocalization S X)

Equations

• OreLocalization.instMulActionOreLocalization = { toSMul := OreLocalization.instSMul, mul_smul := ⋯, one_smul := ⋯ }

instance AddOreLocalization.instAddActionOreLocalization {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] : AddAction (AddOreLocalization S R) (AddOreLocalization S X)

Equations

• AddOreLocalization.instAddActionOreLocalization = { toVAdd := AddOreLocalization.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }

theorem OreLocalization.mul_inv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (s s' : ↥S) : ↑s /ₒ s' * (↑s' /ₒ s) = 1

theorem AddOreLocalization.add_neg {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (s s' : ↥S) : ↑s -ₒ s' + (↑s' -ₒ s) = 0

@[simp]

theorem OreLocalization.one_div_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {r : X} {s t : ↥S} : (1 /ₒ t) • (r /ₒ s) = r /ₒ (s * t)

@[simp]

theorem AddOreLocalization.zero_sub_vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {r : X} {s t : ↥S} : (0 -ₒ t) +ᵥ r -ₒ s = r -ₒ (s + t)

@[simp]

theorem OreLocalization.one_div_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r : R} {s t : ↥S} : 1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)

@[simp]

theorem AddOreLocalization.zero_sub_add {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r : R} {s t : ↥S} : 0 -ₒ t + (r -ₒ s) = r -ₒ (s + t)

@[simp]

theorem OreLocalization.smul_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {r : X} {s t : ↥S} : (↑s /ₒ t) • (r /ₒ s) = r /ₒ t

@[simp]

theorem AddOreLocalization.vadd_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {r : X} {s t : ↥S} : (↑s -ₒ t) +ᵥ r -ₒ s = r -ₒ t

@[simp]

theorem OreLocalization.mul_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r : R} {s t : ↥S} : ↑s /ₒ t * (r /ₒ s) = r /ₒ t

@[simp]

theorem AddOreLocalization.add_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r : R} {s t : ↥S} : ↑s -ₒ t + (r -ₒ s) = r -ₒ t

@[simp]

theorem OreLocalization.smul_cancel' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {r₁ : R} {r₂ : X} {s t : ↥S} : (r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t

@[simp]

theorem AddOreLocalization.vadd_cancel' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ : R} {r₂ : X} {s t : ↥S} : (r₁ + ↑s -ₒ t) +ᵥ r₂ -ₒ s = (r₁ +ᵥ r₂) -ₒ t

@[simp]

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

@[simp]

theorem AddOreLocalization.add_cancel' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r₁ r₂ : R} {s t : ↥S} : r₁ + ↑s -ₒ t + (r₂ -ₒ s) = r₁ + r₂ -ₒ t

@[simp]

theorem OreLocalization.smul_div_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] {p : R} {r : X} {s : ↥S} : (p /ₒ s) • (r /ₒ 1) = p • r /ₒ s

@[simp]

theorem AddOreLocalization.vadd_sub_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] {p : R} {r : X} {s : ↥S} : (p -ₒ s) +ᵥ r -ₒ 0 = (p +ᵥ r) -ₒ s

@[simp]

theorem OreLocalization.mul_div_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {p r : R} {s : ↥S} : p /ₒ s * (r /ₒ 1) = p * r /ₒ s

@[simp]

theorem AddOreLocalization.add_sub_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {p r : R} {s : ↥S} : p -ₒ s + (r -ₒ 0) = p + r -ₒ s

def OreLocalization.numeratorUnit {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (s : ↥S) : (OreLocalization S R)ˣ

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

Equations

• OreLocalization.numeratorUnit s = { val := ↑s /ₒ 1, inv := 1 /ₒ s, val_inv := ⋯, inv_val := ⋯ }

def AddOreLocalization.numeratorAddUnit {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (s : ↥S) : AddUnits (AddOreLocalization S R)

The difference s -ₒ 0 as an additive unit.

Equations

• AddOreLocalization.numeratorAddUnit s = { val := ↑s -ₒ 0, neg := 0 -ₒ s, val_neg := ⋯, neg_val := ⋯ }

@[reducible, inline]

abbrev OreLocalization.numeratorHom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] : R →* OreLocalization S R

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

Equations

• OreLocalization.numeratorHom = { toFun := fun (r : R) => r /ₒ 1, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

abbrev AddOreLocalization.numeratorHom {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] : R →+ AddOreLocalization S R

The additive homomorphism from R to AddOreLocalization R S, mapping r : R to the difference r -ₒ 0.

Equations

• AddOreLocalization.numeratorHom = { toFun := fun (r : R) => r -ₒ 0, map_zero' := ⋯, map_add' := ⋯ }

theorem OreLocalization.numeratorHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r : R} : numeratorHom r = r /ₒ 1

theorem AddOreLocalization.numeratorHom_apply {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r : R} : numeratorHom r = r -ₒ 0

theorem OreLocalization.numerator_isUnit {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (s : ↥S) : IsUnit (numeratorHom ↑s)

theorem AddOreLocalization.numerator_isAddUnit {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (s : ↥S) : IsAddUnit (numeratorHom ↑s)

def OreLocalization.universalMulHom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) : OreLocalization S R →* T

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

Equations

• OreLocalization.universalMulHom f fS hf = { toFun := fun (x : OreLocalization S R) => OreLocalization.liftExpand (fun (r : R) (s : ↥S) => ↑(fS s)⁻¹ * f r) ⋯ x, map_one' := ⋯, map_mul' := ⋯ }

def AddOreLocalization.universalAddHom {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) : AddOreLocalization S R →+ T

The universal lift from a morphism R →+ T, which maps elements of S to additive-units of T, to a morphism AddOreLocalization R S →+ T.

Equations

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

theorem OreLocalization.universalMulHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [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} : (universalMulHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r

theorem AddOreLocalization.universalAddHom_apply {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} {s : ↥S} : (universalAddHom f fS hf) (r -ₒ s) = ↑(-fS s) + f r

theorem OreLocalization.universalMulHom_commutes {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} : (universalMulHom f fS hf) (numeratorHom r) = f r

theorem AddOreLocalization.universalAddHom_commutes {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} : (universalAddHom f fS hf) (numeratorHom r) = f r

theorem OreLocalization.universalMulHom_unique {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : OreLocalization S R →* T) (huniv : ∀ (r : R), φ (numeratorHom r) = f r) : φ = universalMulHom f fS hf

The universal morphism universalMulHom is unique.

theorem AddOreLocalization.universalAddHom_unique {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : AddOreLocalization S R →+ T) (huniv : ∀ (r : R), φ (numeratorHom r) = f r) : φ = universalAddHom f fS hf

The universal morphism universalAddHom is unique.

@[irreducible]

def OreLocalization.hsmul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R M] (c : R) : OreLocalization S X → OreLocalization S X

Scalar multiplication in a monoid localization.

Equations

• OreLocalization.hsmul c = OreLocalization.liftExpand (fun (m : X) (s : ↥S) => OreLocalization.oreNum (c • 1) s • m /ₒ OreLocalization.oreDenom (c • 1) s) ⋯

@[irreducible]

def AddOreLocalization.hvadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R M] (c : R) : AddOreLocalization S X → AddOreLocalization S X

Vector addition in an additive monoid localization.

Equations

• AddOreLocalization.hvadd c = AddOreLocalization.liftExpand (fun (m : X) (s : ↥S) => (AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m) -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) ⋯

instance OreLocalization.instSMulOfIsScalarTower {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M X] [IsScalarTower R M M] : SMul R (OreLocalization S X)

Equations

• OreLocalization.instSMulOfIsScalarTower = { smul := OreLocalization.hsmul }

instance AddOreLocalization.instVAddOfVAddAssocClass {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M X] [VAddAssocClass R M M] : VAdd R (AddOreLocalization S X)

Equations

• AddOreLocalization.instVAddOfVAddAssocClass = { vadd := AddOreLocalization.hvadd }

theorem OreLocalization.smul_oreDiv {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : X) (s : ↥S) : r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

theorem AddOreLocalization.vadd_oreSub {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : X) (s : ↥S) : r +ᵥ x -ₒ s = (oreMin (r +ᵥ 0) s +ᵥ x) -ₒ oreSubtra (r +ᵥ 0) s

@[simp]

theorem OreLocalization.oreDiv_one_smul {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] (r : M) (x : OreLocalization S X) : (r /ₒ 1) • x = r • x

@[simp]

theorem AddOreLocalization.oreSub_zero_vadd {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] (r : M) (x : AddOreLocalization S X) : (r -ₒ 0) +ᵥ x = r +ᵥ x

theorem OreLocalization.smul_one_smul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : OreLocalization S X) : (r • 1) • x = r • x

theorem AddOreLocalization.vadd_zero_vadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : AddOreLocalization S X) : (r +ᵥ 0) +ᵥ x = r +ᵥ x

theorem OreLocalization.smul_one_oreDiv_one_smul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : OreLocalization S X) : (r • 1 /ₒ 1) • x = r • x

theorem AddOreLocalization.vadd_zero_oreSub_zero_vadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : AddOreLocalization S X) : ((r +ᵥ 0) -ₒ 0) +ᵥ x = r +ᵥ x

instance OreLocalization.instIsScalarTower {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul R' X] [SMul R' M] [IsScalarTower R' M M] [IsScalarTower R' M X] [SMul R R'] [IsScalarTower R R' M] : IsScalarTower R R' (OreLocalization S X)

instance AddOreLocalization.instVAddAssocClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] [VAdd R' X] [VAdd R' M] [VAddAssocClass R' M M] [VAddAssocClass R' M X] [VAdd R R'] [VAddAssocClass R R' M] : VAddAssocClass R R' (AddOreLocalization S X)

instance OreLocalization.instSMulCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul R' X] [SMul R' M] [IsScalarTower R' M M] [IsScalarTower R' M X] [SMulCommClass R R' M] : SMulCommClass R R' (OreLocalization S X)

instance AddOreLocalization.instVAddCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] [VAdd R' X] [VAdd R' M] [VAddAssocClass R' M M] [VAddAssocClass R' M X] [VAddCommClass R R' M] : VAddCommClass R R' (AddOreLocalization S X)

instance OreLocalization.instIsScalarTower_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] : IsScalarTower R (OreLocalization S M) (OreLocalization S X)

instance AddOreLocalization.instVAddAssocClass_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] : VAddAssocClass R (AddOreLocalization S M) (AddOreLocalization S X)

instance OreLocalization.instSMulCommClass_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMulCommClass R M M] : SMulCommClass R (OreLocalization S M) (OreLocalization S X)

instance AddOreLocalization.instVAddCommClass_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] [VAddCommClass R M M] : VAddCommClass R (AddOreLocalization S M) (AddOreLocalization S X)

instance OreLocalization.instIsCentralScalar {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul Rᵐᵒᵖ M] [SMul Rᵐᵒᵖ X] [IsScalarTower Rᵐᵒᵖ M M] [IsScalarTower Rᵐᵒᵖ M X] [IsCentralScalar R M] : IsCentralScalar R (OreLocalization S X)

instance AddOreLocalization.instIsCentralVAdd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] [VAdd Rᵃᵒᵖ M] [VAdd Rᵃᵒᵖ X] [VAddAssocClass Rᵃᵒᵖ M M] [VAddAssocClass Rᵃᵒᵖ M X] [IsCentralVAdd R M] : IsCentralVAdd R (AddOreLocalization S X)

instance OreLocalization.instMulActionOfIsScalarTower {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] {R : Type u_5} [Monoid R] [MulAction R M] [IsScalarTower R M M] [MulAction R X] [IsScalarTower R M X] : MulAction R (OreLocalization S X)

Equations

• OreLocalization.instMulActionOfIsScalarTower = { toSMul := OreLocalization.instSMulOfIsScalarTower, mul_smul := ⋯, one_smul := ⋯ }

instance AddOreLocalization.instAddActionOfVAddAssocClass {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] {R : Type u_5} [AddMonoid R] [AddAction R M] [VAddAssocClass R M M] [AddAction R X] [VAddAssocClass R M X] : AddAction R (AddOreLocalization S X)

Equations

• AddOreLocalization.instAddActionOfVAddAssocClass = { toVAdd := AddOreLocalization.instVAddOfVAddAssocClass, add_vadd := ⋯, zero_vadd := ⋯ }

theorem OreLocalization.smul_oreDiv_one {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : X) : r • (x /ₒ 1) = r • x /ₒ 1

theorem AddOreLocalization.vadd_oreSub_zero {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : X) : r +ᵥ x -ₒ 0 = (r +ᵥ x) -ₒ 0

theorem OreLocalization.oreDiv_mul_oreDiv_comm {R : Type u_1} [CommMonoid R] {S : Submonoid R} [OreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S} : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)

theorem AddOreLocalization.oreSub_add_oreSub_comm {R : Type u_1} [AddCommMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S} : r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r₁ + r₂ -ₒ (s₁ + s₂)

instance OreLocalization.instCommMonoid {R : Type u_1} [CommMonoid R] {S : Submonoid R} [OreSet S] : CommMonoid (OreLocalization S R)

Equations

• OreLocalization.instCommMonoid = { toMonoid := OreLocalization.instMonoid, mul_comm := ⋯ }

instance AddOreLocalization.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] {S : AddSubmonoid R} [AddOreSet S] : AddCommMonoid (AddOreLocalization S R)

Equations

• AddOreLocalization.instAddCommMonoid = { toAddMonoid := AddOreLocalization.instAddMonoid, add_comm := ⋯ }

@[irreducible]

def OreLocalization.zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [Zero X] [MulAction R X] : OreLocalization S X

0 in the localization, defined as 0 /ₒ 1.

Equations

• OreLocalization.zero = 0 /ₒ 1

instance OreLocalization.instZero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [Zero X] [MulAction R X] : Zero (OreLocalization S X)

Equations

• OreLocalization.instZero = { zero := OreLocalization.zero }

theorem OreLocalization.zero_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [Zero X] [MulAction R X] : 0 = 0 /ₒ 1