Localization over left Ore sets.

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

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

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

Tags

localization, Ore, non-commutative

def AddOreLocalization.oreEqv {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) [AddOreLocalization.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 := ⋯ }

theorem AddOreLocalization.oreEqv.proof_1 {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) [AddOreLocalization.AddOreSet S] (X : Type u_2) [AddAction R X] : Equivalence fun (rs rs' : X × ↥S) => ∃ (u : ↥S) (v : R), u +ᵥ rs'.1 = v +ᵥ rs.1 ∧ ↑u + ↑rs'.2 = v + ↑rs.2

def OreLocalization.oreEqv {R : Type u_1} [Monoid R] (S : Submonoid R) [OreLocalization.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 {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 {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 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 AddOreLocalization.oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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.oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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 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 AddOreLocalization.ind {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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.ind {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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.oreSub_eq_iff {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ : X} {r₂ : X} {s₁ : ↥S} {s₂ : ↥S} : r₁ -ₒ s₁ = r₂ -ₒ s₂ ↔ ∃ (u : ↥S) (v : R), u +ᵥ r₂ = v +ᵥ r₁ ∧ ↑u + ↑s₂ = v + ↑s₁

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

theorem AddOreLocalization.expand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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} [OreLocalization.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} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s : ↥S) (s' : ↥S) : r -ₒ s = s' +ᵥ r -ₒ (s' + s)

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

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

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

theorem AddOreLocalization.eq_of_num_factor_eq {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r : R} {r' : R} {r₁ : R} {r₂ : R} {s : ↥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.

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 : ↑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.

abbrev AddOreLocalization.liftExpand.match_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S) (motive : (r₁, s₁) ≈ (r₂, s₂) → Prop) : ∀ (x : (r₁, s₁) ≈ (r₂, s₂)), (∀ (u : ↥S) (v : R) (hr₂ : u +ᵥ (r₂, s₂).1 = v +ᵥ (r₁, s₁).1) (hs₂ : ↑u + ↑(r₂, s₂).2 = v + ↑(r₁, s₁).2), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddOreLocalization.liftExpand.match_3 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] : ∀ (x : X × ↥S) (motive : (x_1 : X × ↥S) → x_1 ≈ x → Prop) (x_1 : X × ↥S) (x_2 : x_1 ≈ x), (∀ (r₁ : X) (s₁ : ↥S) (x : (r₁, s₁) ≈ x), motive (r₁, s₁) x) → motive x_1 x_2

Equations

• ⋯ = ⋯

theorem AddOreLocalization.liftExpand.proof_1 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] {C : Sort u_3} (P : X → ↥S → C) (hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩) : ∀ (x x_1 : X × ↥S), x ≈ x_1 → (fun (p : X × ↥S) => P p.1 p.2) x = (fun (p : X × ↥S) => P p.1 p.2) x_1

abbrev AddOreLocalization.liftExpand.match_2 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] (r₁ : X) (s₁ : ↥S) (motive : (x : X × ↥S) → (r₁, s₁) ≈ x → Prop) : ∀ (x : X × ↥S) (x_1 : (r₁, s₁) ≈ x), (∀ (r₂ : X) (s₂ : ↥S) (x : (r₁, s₁) ≈ (r₂, s₂)), motive (r₂, s₂) x) → motive x x_1

Equations

• ⋯ = ⋯

def AddOreLocalization.liftExpand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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 localizaton 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) ⋯

def OreLocalization.liftExpand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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) ⋯

@[simp]

theorem AddOreLocalization.liftExpand_of {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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) : AddOreLocalization.liftExpand P hP (r -ₒ s) = P r s

@[simp]

theorem OreLocalization.liftExpand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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) : OreLocalization.liftExpand P hP (r /ₒ s) = P r s

theorem AddOreLocalization.lift₂Expand.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} {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) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S) : P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩

def AddOreLocalization.lift₂Expand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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₁) ⋯) ⋯

theorem AddOreLocalization.lift₂Expand.proof_2 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {C : Sort u_3} (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) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) : (fun (r₁ : X) (s₁ : ↥S) => AddOreLocalization.liftExpand (P r₁ s₁) ⋯) r₁ s₁ = (fun (r₁ : X) (s₁ : ↥S) => AddOreLocalization.liftExpand (P r₁ s₁) ⋯) (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩

def OreLocalization.lift₂Expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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₁) ⋯) ⋯

@[simp]

theorem AddOreLocalization.lift₂Expand_of {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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) : AddOreLocalization.lift₂Expand P hP (r₁ -ₒ s₁) (r₂ -ₒ s₂) = P r₁ s₁ r₂ s₂

@[simp]

theorem OreLocalization.lift₂Expand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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) : OreLocalization.lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂

theorem AddOreLocalization.vadd.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : R) (s : ↥S) (hs : r₂ + ↑s ∈ S) : OreLocalization.vadd'' r₁ s = OreLocalization.vadd'' (r₂ +ᵥ r₁) ⟨r₂ + ↑s, hs⟩

def AddOreLocalization.vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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'' ⋯

def OreLocalization.smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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'' ⋯

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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₂) = OreLocalization.oreNum r₁ s₂ * r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)

theorem AddOreLocalization.oreSub_vadd_char {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ : ↥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_smul_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r₁ : R) (r₂ : X) (s₁ : ↥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_add_char {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s₁ : ↥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.

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 : ↑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.

def AddOreLocalization.oreSubVAddChar' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ : ↥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 localizaion 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₂, ⋯⟩⟩

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

def OreLocalization.oreDivSMulChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r₁ : R) (r₂ : X) (s₁ : ↥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 localizaion 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₂, ⋯⟩⟩

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

def AddOreLocalization.oreSubAddChar' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s₁ : ↥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 localizaion 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₂, ⋯⟩⟩

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) ×' ↑s' * r₁ = r' * ↑s₂ ∧ 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

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

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

Equations

• AddOreLocalization.instZeroAddOreLocalization = { zero := 0 -ₒ 0 }

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

Equations

• OreLocalization.instOne = { one := 1 /ₒ 1 }

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

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

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

Equations

• AddOreLocalization.instInhabited = { default := 0 }

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

Equations

• OreLocalization.instInhabited = { default := 1 }

@[simp]

theorem AddOreLocalization.sub_eq_zero' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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} [OreLocalization.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} [AddOreLocalization.AddOreSet S] {s : ↥S} : ↑s -ₒ s = 0

@[simp]

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

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

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

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

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

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

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

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

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

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

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

theorem AddOreLocalization.instAddMonoid.proof_2 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] : ∀ (n : ℕ) (x : AddOreLocalization S R), nsmulRec (n + 1) x = nsmulRec (n + 1) x

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

Equations

• AddOreLocalization.instAddMonoid = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

theorem AddOreLocalization.instAddMonoid.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] : ∀ (x : AddOreLocalization S R), nsmulRec 0 x = nsmulRec 0 x

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

Equations

• OreLocalization.instMonoid = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

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

Equations

• AddOreLocalization.instAddActionOreLocalization = AddAction.mk ⋯ ⋯

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

Equations

• OreLocalization.instMulActionOreLocalization = MulAction.mk ⋯ ⋯

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

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 AddOreLocalization.zero_sub_vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r : X} {s : ↥S} {t : ↥S} : 0 -ₒ t +ᵥ (r -ₒ s) = r -ₒ (s + t)

@[simp]

theorem OreLocalization.one_div_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r : X} {s : ↥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} [AddOreLocalization.AddOreSet S] {r : R} {s : ↥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} [OreLocalization.OreSet S] {r : R} {s : ↥S} {t : ↥S} : 1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem OreLocalization.smul_cancel' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r₁ : R} {r₂ : X} {s : ↥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} [AddOreLocalization.AddOreSet S] {r₁ : R} {r₂ : R} {s : ↥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} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s : ↥S} {t : ↥S} : r₁ * ↑s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t

@[simp]

theorem AddOreLocalization.vadd_sub_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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.smul_div_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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.add_sub_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {p : R} {r : R} {s : ↥S} : p -ₒ s + (r -ₒ 0) = p + r -ₒ s

@[simp]

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

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

Equations

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

theorem AddOreLocalization.instVAdd_1.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r : R) (x : X) (r' : R) (s : ↥S) (h : r' + ↑s ∈ S) : (fun (x : X) (s : ↥S) => AddOreLocalization.oreMin r s +ᵥ x -ₒ AddOreLocalization.oreSubtra r s) x s = (fun (x : X) (s : ↥S) => AddOreLocalization.oreMin r s +ᵥ x -ₒ AddOreLocalization.oreSubtra r s) (r' +ᵥ x) ⟨r' + ↑s, h⟩

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

Equations

• OreLocalization.instSMul_1 = { smul := fun (r : R) => OreLocalization.liftExpand (fun (x : X) (s : ↥S) => OreLocalization.oreNum r s • x /ₒ OreLocalization.oreDenom r s) ⋯ }

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

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

@[simp]

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

@[simp]

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

theorem AddOreLocalization.instAddAction.proof_2 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] (r : R) (r' : R) (q : AddOreLocalization S X) : r + r' +ᵥ q = r +ᵥ (r' +ᵥ q)

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

Equations

• AddOreLocalization.instAddAction = AddAction.mk ⋯ ⋯

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

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

Equations

• OreLocalization.instMulAction = MulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

def AddOreLocalization.numeratorAddUnit {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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 := ⋯ }

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

def OreLocalization.numeratorUnit {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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 := ⋯ }

theorem AddOreLocalization.numeratorHom.proof_2 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] : ∀ (x x_1 : R), x + x_1 -ₒ 0 = x -ₒ 0 + (x_1 -ₒ 0)

theorem AddOreLocalization.numeratorHom.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] : (fun (r : R) => r -ₒ 0) 0 = (fun (r : R) => r -ₒ 0) 0

def AddOreLocalization.numeratorHom {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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' := ⋯ }

def OreLocalization.numeratorHom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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' := ⋯ }

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

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

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

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

theorem AddOreLocalization.universalAddHom.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (r : R) (t : R) (s : ↥S) (ht : t + ↑s ∈ S) : (fun (r : R) (s : ↥S) => ↑(-fS s) + f r) r s = (fun (r : R) (s : ↥S) => ↑(-fS s) + f r) (t +ᵥ r) ⟨t + ↑s, ht⟩

theorem AddOreLocalization.universalAddHom.proof_2 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_1} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) : (fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : ↥S) => ↑(-fS s) + f r) ⋯ x) 0 = 0

theorem AddOreLocalization.universalAddHom.proof_3 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (x : AddOreLocalization S R) (y : AddOreLocalization S R) : { toFun := fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : ↥S) => ↑(-fS s) + f r) ⋯ x, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : ↥S) => ↑(-fS s) + f r) ⋯ x, map_zero' := ⋯ }.toFun x + { toFun := fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : ↥S) => ↑(-fS s) + f r) ⋯ x, map_zero' := ⋯ }.toFun y

def AddOreLocalization.universalAddHom {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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.

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

theorem AddOreLocalization.universalAddHom_apply {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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} : (AddOreLocalization.universalAddHom f fS hf) (r -ₒ s) = ↑(-fS s) + f r

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) = ↑(fS s)⁻¹ * f r

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

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 AddOreLocalization.universalAddHom_unique {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.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), φ (AddOreLocalization.numeratorHom r) = f r) : φ = AddOreLocalization.universalAddHom f fS hf

The universal morphism universalAddHom is unique.

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 S R →* T) (huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) : φ = OreLocalization.universalMulHom f fS hf

The universal morphism universalMulHom is unique.

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

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

theorem AddOreLocalization.instAddCommMonoid.proof_1 {R : Type u_1} [AddCommMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (x : AddOreLocalization S R) (y : AddOreLocalization S R) : x + y = y + x

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

Equations

• AddOreLocalization.instAddCommMonoid = AddCommMonoid.mk ⋯

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

Equations

• OreLocalization.instCommMonoid = CommMonoid.mk ⋯

instance OreLocalization.instAdd {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : Add (OreLocalization S X)

Equations

• OreLocalization.instAdd = { add := OreLocalization.add }

theorem OreLocalization.oreDiv_add_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} {s : ↥S} {s' : ↥S} : r /ₒ s + r' /ₒ s' = (OreLocalization.oreDenom (↑s) s' • r + OreLocalization.oreNum (↑s) s' • r') /ₒ (OreLocalization.oreDenom (↑s) s' * s)

theorem OreLocalization.oreDiv_add_char' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} (s : ↥S) (s' : ↥S) (rb : R) (sb : R) (h : sb * ↑s = rb * ↑s') (h' : sb * ↑s ∈ S) : r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩

theorem OreLocalization.oreDiv_add_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} (s : ↥S) (s' : ↥S) (rb : R) (sb : ↥S) (h : ↑sb * ↑s = rb * ↑s') : r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s)

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

def OreLocalization.oreDivAddChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (r : X) (r' : X) (s : ↥S) (s' : ↥S) : (r'' : R) ×' (s'' : ↥S) ×' ↑s'' * ↑s = r'' * ↑s' ∧ r /ₒ s + r' /ₒ s' = (s'' • r + r'' • r') /ₒ (s'' * s)

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

Equations

• OreLocalization.oreDivAddChar' r r' s s' = ⟨OreLocalization.oreNum (↑s) s', ⟨OreLocalization.oreDenom (↑s) s', ⋯⟩⟩

@[simp]

theorem OreLocalization.add_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} {s : ↥S} : r /ₒ s + r' /ₒ s = (r + r') /ₒ s

theorem OreLocalization.add_assoc {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) (y : OreLocalization S X) (z : OreLocalization S X) : x + y + z = x + (y + z)

instance OreLocalization.instZero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction 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} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : 0 = 0 /ₒ 1

@[simp]

theorem OreLocalization.zero_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (s : ↥S) : 0 /ₒ s = 0

theorem OreLocalization.zero_add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) : 0 + x = x

theorem OreLocalization.add_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) : x + 0 = x

instance OreLocalization.instAddMonoid {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : AddMonoid (OreLocalization S X)

Equations

• OreLocalization.instAddMonoid = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

theorem OreLocalization.smul_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S R) : x • 0 = 0

theorem OreLocalization.smul_add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (z : OreLocalization S R) (x : OreLocalization S X) (y : OreLocalization S X) : z • (x + y) = z • x + z • y

instance OreLocalization.instDistribMulAction {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : DistribMulAction (OreLocalization S R) (OreLocalization S X)

Equations

• OreLocalization.instDistribMulAction = DistribMulAction.mk ⋯ ⋯

instance OreLocalization.instDistribMulAction_1 {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : DistribMulAction R (OreLocalization S X)

Equations

• OreLocalization.instDistribMulAction_1 = DistribMulAction.mk ⋯ ⋯

theorem OreLocalization.add_comm {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommMonoid X] [DistribMulAction R X] (x : OreLocalization S X) (y : OreLocalization S X) : x + y = y + x

instance OreLocalization.instAddCommMonoidOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommMonoid X] [DistribMulAction R X] : AddCommMonoid (OreLocalization S X)

Equations

• OreLocalization.instAddCommMonoidOreLocalization = AddCommMonoid.mk ⋯

def OreLocalization.neg {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] : OreLocalization S X → OreLocalization S X

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

Equations

• OreLocalization.neg = OreLocalization.liftExpand (fun (r : X) (s : ↥S) => -r /ₒ s) ⋯

instance OreLocalization.instNegOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] : Neg (OreLocalization S X)

Equations

• OreLocalization.instNegOreLocalization = { neg := OreLocalization.neg }

@[simp]

theorem OreLocalization.neg_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] (r : X) (s : ↥S) : -(r /ₒ s) = -r /ₒ s

theorem OreLocalization.add_left_neg {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] (x : OreLocalization S X) : -x + x = 0

instance OreLocalization.instAddGroupOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] : AddGroup (OreLocalization S X)

Equations

• OreLocalization.instAddGroupOreLocalization = AddGroup.mk ⋯

instance OreLocalization.instAddCommGroup {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommGroup X] [DistribMulAction R X] : AddCommGroup (OreLocalization S X)

Equations

• OreLocalization.instAddCommGroup = let __spread.0 := inferInstanceAs (AddGroup (OreLocalization S X)); let __spread.1 := inferInstanceAs (AddCommMonoid (OreLocalization S X)); AddCommGroup.mk ⋯