# 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

source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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
source
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
source
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₁
source
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₁
source
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`.

source
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`.

source
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`.

source
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`.

source
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`.

source
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`.

source
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) ⋯

Instances For

source
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) ⋯

Instances For

source
@[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
source
@[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
source
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₁) ⋯) ⋯

Instances For

source
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₁) ⋯) ⋯

Instances For

source
@[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₂
source
@[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₂
source
@[irreducible]
def OreLocalization.smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [MulAction R X] :
OreLocalization S R → OreLocalization S X → OreLocalization S X

The scalar multiplication on the Ore localization of monoids.

Equations

- OreLocalization.smul = OreLocalization.liftExpand OreLocalization.smul''✝ ⋯

Instances For

source
@[irreducible]
def AddOreLocalization.vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {X : Type u_2} [AddAction R X] :
AddOreLocalization S R → AddOreLocalization S X → AddOreLocalization S X

the vector addition on the Ore localization of additive monoids.

Equations

- AddOreLocalization.vadd = AddOreLocalization.liftExpand OreLocalization.vadd''✝ ⋯

Instances For

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

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

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

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

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

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

source
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₁)
source
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₁)
source
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₁)
source
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₁)
source
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.

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

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

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

source
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₂, ⋯⟩⟩

Instances For

source
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₂, ⋯⟩⟩

Instances For

source
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₂, ⋯⟩⟩

Instances For

source
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₂, ⋯⟩⟩

Instances For

source
@[irreducible]
def OreLocalization.one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] :
OreLocalization S R

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

Equations

- OreLocalization.one = 1 /ₒ 1

Instances For

source
@[irreducible]
def AddOreLocalization.zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] :
AddOreLocalization S R

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

Equations

- AddOreLocalization.zero = 0 -ₒ 0

Instances For

source
instance OreLocalization.instOne {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] :
One (OreLocalization S R)
Equations

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

source
instance AddOreLocalization.instZero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] :
Zero (AddOreLocalization S R)
Equations

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

source
theorem OreLocalization.one_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] :
1 = 1 /ₒ 1
source
theorem AddOreLocalization.zero_def {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] :
0 = 0 -ₒ 0
source
instance OreLocalization.instInhabited {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] :
Inhabited (OreLocalization S R)
Equations

- OreLocalization.instInhabited = { default := 1 }

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

- AddOreLocalization.instInhabited = { default := 0 }

source
@[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
source
@[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
source
@[simp]
theorem OreLocalization.div_eq_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {s : ↥S} :
↑s /ₒ s = 1
source
@[simp]
theorem AddOreLocalization.sub_eq_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {s : ↥S} :
↑s -ₒ s = 0
source
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
source
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
source
theorem OreLocalization.one_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (x : OreLocalization S R) :
1 * x = x
source
theorem AddOreLocalization.zero_add {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (x : AddOreLocalization S R) :
0 + x = x
source
theorem OreLocalization.mul_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (x : OreLocalization S R) :
x * 1 = x
source
theorem AddOreLocalization.add_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (x : AddOreLocalization S R) :
x + 0 = x
source
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
source
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
source
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)
source
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)
source
@[irreducible]
def 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

Instances For

source
@[irreducible]
def 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

Instances For

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

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

source
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, one_smul := ⋯, mul_smul := ⋯ }

source
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, zero_vadd := ⋯, add_vadd := ⋯ }

source
theorem OreLocalization.mul_inv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (s s' : ↥S) :
↑s /ₒ s' * (↑s' /ₒ s) = 1
source
theorem AddOreLocalization.add_neg {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (s s' : ↥S) :
↑s -ₒ s' + (↑s' -ₒ s) = 0
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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 := ⋯ }

Instances For

source
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 a an additive unit.

Equations

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

Instances For

source
def 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' := ⋯ }

Instances For

source
def 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' := ⋯ }

Instances For

source
theorem OreLocalization.numeratorHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {r : R} :
numeratorHom r = r /ₒ 1
source
theorem AddOreLocalization.numeratorHom_apply {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] {r : R} :
numeratorHom r = r -ₒ 0
source
theorem OreLocalization.numerator_isUnit {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] (s : ↥S) :
IsUnit (numeratorHom ↑s)
source
theorem AddOreLocalization.numerator_isAddUnit {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreSet S] (s : ↥S) :
IsAddUnit (numeratorHom ↑s)
source
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' := ⋯ }

Instances For

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

Instances For

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

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

source
@[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) ⋯

Instances For

source
@[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) ⋯

Instances For

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

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

source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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, one_smul := ⋯, mul_smul := ⋯ }

source
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, zero_vadd := ⋯, add_vadd := ⋯ }

source
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
source
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
source
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₂)
source
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₂)
source
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 := ⋯ }

source
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 := ⋯ }

source
@[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

Instances For

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

source
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