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.

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

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

@[irreducible]

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

@[irreducible]

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.

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

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

@[irreducible]

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

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

Equations

• AddOreLocalization.zero = 0 -ₒ 0

@[irreducible]

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

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

Equations

• OreLocalization.one = 1 /ₒ 1

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

Equations

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

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

Equations

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

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)

@[irreducible]

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

nsmul of AddOreLocalization

Equations

• AddOreLocalization.nsmul = nsmulRec

@[irreducible]

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

npow of OreLocalization

Equations

• OreLocalization.npow = npowRec

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

theorem AddOreLocalization.instAddMonoid.proof_2 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] : ∀ (n : ℕ) (x : AddOreLocalization S R), AddOreLocalization.nsmul (n + 1) x = AddOreLocalization.nsmul (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 ⋯ ⋯ AddOreLocalization.nsmul ⋯ ⋯

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

Equations

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

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

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

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

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

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)

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

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

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.

@[irreducible]

def AddOreLocalization.hvadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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) ⋯

theorem AddOreLocalization.hvadd.proof_1 {R : Type u_3} {M : Type u_1} {X : Type u_2} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R M] (c : R) (r : X) (t : M) (s : ↥S) (ht : t + ↑s ∈ S) : (fun (m : X) (s : ↥S) => AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) r s = (fun (m : X) (s : ↥S) => AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) (t +ᵥ r) ⟨t + ↑s, ht⟩

@[irreducible]

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

instance AddOreLocalization.instVAddOfIsScalarTower {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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.instVAddOfIsScalarTower = { vadd := AddOreLocalization.hvadd }

instance OreLocalization.instSMulOfIsScalarTower {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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 }

theorem AddOreLocalization.vadd_oreSub {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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) = AddOreLocalization.oreMin (r +ᵥ 0) s +ᵥ x -ₒ AddOreLocalization.oreSubtra (r +ᵥ 0) s

theorem OreLocalization.smul_oreDiv {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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) = OreLocalization.oreNum (r • 1) s • x /ₒ OreLocalization.oreDenom (r • 1) s

@[simp]

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

@[simp]

theorem OreLocalization.oreDiv_one_smul {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] (r : M) (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} [AddOreLocalization.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_smul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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_oreSub_zero_vadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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

theorem OreLocalization.smul_one_oreDiv_one_smul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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

instance AddOreLocalization.instIsScalarTower {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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)

Equations

• ⋯ = ⋯

instance OreLocalization.instIsScalarTower {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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)

Equations

• ⋯ = ⋯

instance AddOreLocalization.instVAddCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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)

Equations

• ⋯ = ⋯

instance OreLocalization.instSMulCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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)

Equations

• ⋯ = ⋯

instance AddOreLocalization.instIsScalarTower_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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)

Equations

• ⋯ = ⋯

instance OreLocalization.instIsScalarTower_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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)

Equations

• ⋯ = ⋯

instance AddOreLocalization.instVAddCommClass_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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)

Equations

• ⋯ = ⋯

instance OreLocalization.instSMulCommClass_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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)

Equations

• ⋯ = ⋯

instance AddOreLocalization.instIsCentralVAdd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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)

Equations

• ⋯ = ⋯

instance OreLocalization.instIsCentralScalar {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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)

Equations

• ⋯ = ⋯

instance AddOreLocalization.instAddActionOfIsScalarTower {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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.instAddActionOfIsScalarTower = AddAction.mk ⋯ ⋯

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

theorem AddOreLocalization.instAddActionOfIsScalarTower.proof_2 {M : Type u_1} {X : Type u_2} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] {R : Type u_3} [AddMonoid R] [AddAction R M] [VAddAssocClass R M M] [AddAction R X] [VAddAssocClass R M X] (s₁ : R) (s₂ : R) (x : AddOreLocalization S X) : s₁ + s₂ +ᵥ x = s₁ +ᵥ (s₂ +ᵥ x)

instance OreLocalization.instMulActionOfIsScalarTower {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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 = MulAction.mk ⋯ ⋯

theorem AddOreLocalization.vadd_oreSub_zero {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.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.smul_oreDiv_one {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.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.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₂)

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

Equations

• AddOreLocalization.instAddCommMonoid = AddCommMonoid.mk ⋯

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 OreLocalization.instCommMonoid {R : Type u_1} [CommMonoid R] {S : Submonoid R} [OreLocalization.OreSet S] : CommMonoid (OreLocalization S R)

Equations

• OreLocalization.instCommMonoid = CommMonoid.mk ⋯

@[irreducible]

def OreLocalization.zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.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} [OreLocalization.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} [OreLocalization.OreSet S] {X : Type u_2} [Zero X] [MulAction R X] : 0 = 0 /ₒ 1