Mathlib.GroupTheory.OreLocalization.Basic

OreLocalization.oreEqv definition

: Setoid (X × S)

Full source

/-- The setoid on `R × S` used for the Ore localization. -/
@[to_additive AddOreLocalization.oreEqv "The setoid on `R × S` used for the Ore localization."]
def oreEqv : Setoid (X × S) where
  r rs rs' := ∃ (u : S) (v : R), u • rs'.1 = v • rs.1 ∧ u * rs'.2 = v * rs.2
  iseqv := by
    refine ⟨fun _ => ⟨1, 1, by simp⟩, ?_, ?_⟩
    · rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨u, v, hru, hsu⟩; dsimp only at *
      rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩
      rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩
      have : r₃ * v * s = s₃ * s₂ * s := by
        -- Porting note: the proof used `assoc_rw`
        rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
      rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩
      refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩ <;>
        simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
      · simp only [mul_smul, hru, ← Submonoid.smul_def]
      · simp only [mul_assoc, hsu]
    · rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨r₃, s₃⟩ ⟨u, v, hur₁, hs₁u⟩ ⟨u', v', hur₂, hs₂u⟩
      rcases oreCondition v' u with ⟨r', s', h⟩; dsimp only at *
      refine ⟨s' * u', r' * v, ?_, ?_⟩ <;>
        simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *
      · rw [hur₂, smul_smul, h, mul_smul, hur₁]
      · rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]

Ore localization equivalence relation

Informal description

The equivalence relation on $X \times S$ used for the Ore localization, where $(r, s) \sim (r', s')$ if there exist $u \in S$ and $v \in R$ such that $u \cdot r' = v \cdot r$ and $u \cdot s' = v \cdot s$. Here $R$ is a monoid, $S$ is a submonoid of $R$ that is a left Ore set, and $X$ is a type with a multiplicative action of $R$.

OreLocalization definition

{R : Type*} [Monoid R] (S : Submonoid R) [OreSet S] (X : Type*) [MulAction R X]

Full source

/-- The Ore localization of a monoid and a submonoid fulfilling the Ore condition. -/
@[to_additive AddOreLocalization "The Ore localization of an additive monoid and a submonoid
fulfilling the Ore condition."]
def OreLocalization {R : Type*} [Monoid R] (S : Submonoid R) [OreSet S]
    (X : Type*) [MulAction R X] :=
  Quotient (OreLocalization.oreEqv S X)

Ore localization of a monoid at a left Ore set

Informal description

Given a monoid $R$ and a submonoid $S$ of $R$ satisfying the left Ore condition, the Ore localization $R[S^{-1}]$ is defined as the quotient of $R \times S$ by the equivalence relation $(r, s) \sim (r', s')$ if there exist $u \in S$ and $v \in R$ such that $u \cdot r' = v \cdot r$ and $u \cdot s' = v \cdot s$. This construction extends to any type $X$ with a multiplicative action of $R$.

OreLocalization.term__[_⁻¹_] definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc OreLocalization]
scoped syntax:1075 term noWs atomic("[" term "⁻¹" noWs "]") : term

Ore localization notation `R[S⁻¹]` and division `r /ₒ s`

Informal description

The notation `R[S⁻¹]` represents the Ore localization of a monoid `R` at a right Ore subset `S`. Additionally, the heterogeneous division notation `r /ₒ s` is defined for a numerator `r : R` and denominator `s : S`, where `r /ₒ s` is an element of the Ore localization `R[S⁻¹]`.

OreLocalization.oreDiv definition

(r : X) (s : S) : X[S⁻¹]

Full source

/-- The division in the Ore localization `X[S⁻¹]`, as a fraction of an element of `X` and `S`. -/
@[to_additive "The subtraction in the Ore localization,
as a difference of an element of `X` and `S`."]
def oreDiv (r : X) (s : S) : X[S⁻¹] :=
  Quotient.mk' (r, s)

Ore division of an element by a denominator

Informal description

The division operation in the Ore localization $X[S^{-1}]$ is defined as the equivalence class of the pair $(r, s)$ under the Ore equivalence relation, where $r \in X$ is an element and $s \in S$ is a denominator from the left Ore set $S$.

OreLocalization.term_/ₒ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:70 " /ₒ " => oreDiv

Ore localization fraction notation

Informal description

The notation `r /ₒ s` represents the Ore localization of an element `r` in a monoid `X` with respect to a left Ore subset `S`, where `s` is an element of `S`. This notation is used to denote the fraction `r/s` in the Ore localization of `X` at `S`.

OreLocalization.term_-ₒ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:65 " -ₒ " => _root_.AddOreLocalization.oreSub

Subtraction in additive Ore localization

Informal description

The notation `a -ₒ b` represents the subtraction operation in the additive Ore localization of a monoid, where `a` and `b` are elements of the localized structure.

OreLocalization.ind theorem

{β : X[S⁻¹] → Prop} (c : ∀ (r : X) (s : S), β (r /ₒ s)) : ∀ q, β q

Full source

@[to_additive (attr := elab_as_elim, cases_eliminator, induction_eliminator)]
protected theorem ind {β : X[S⁻¹] → Prop}
    (c : ∀ (r : X) (s : S), β (r /ₒ s)) : ∀ q, β q := by
  apply Quotient.ind
  rintro ⟨r, s⟩
  exact c r s

Induction Principle for Ore Localization

Informal description

For any predicate $\beta$ on the Ore localization $X[S^{-1}]$, if $\beta$ holds for all elements of the form $r /ₒ s$ where $r \in X$ and $s \in S$, then $\beta$ holds for all elements of $X[S^{-1}]$.

OreLocalization.oreDiv_eq_iff theorem

 {r₁ r₂ : X} {s₁ s₂ : S} : r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ (u : S) (v : R), u • r₂ = v • r₁ ∧ u * s₂ = v * s₁

Full source

@[to_additive]
theorem oreDiv_eq_iff {r₁ r₂ : X} {s₁ s₂ : S} :
    r₁ /ₒ s₁r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ (u : S) (v : R), u • r₂ = v • r₁ ∧ u * s₂ = v * s₁ :=
  Quotient.eq''

Equality Criterion for Ore Division: $r_1 /_o s_1 = r_2 /_o s_2$

Informal description

For any elements $r_1, r_2$ in a type $X$ with a multiplicative action of a monoid $R$, and any denominators $s_1, s_2$ in a left Ore set $S \subseteq R$, the Ore division expressions $r_1 /_o s_1$ and $r_2 /_o s_2$ are equal if and only if there exist elements $u \in S$ and $v \in R$ such that: $$u \cdot r_2 = v \cdot r_1 \quad \text{and} \quad u \cdot s_2 = v \cdot s_1.$$

OreLocalization.expand theorem

(r : X) (s : S) (t : R) (hst : t * (s : R) ∈ S) : r /ₒ s = t • r /ₒ ⟨t * s, hst⟩

Full source

/-- A fraction `r /ₒ s` is equal to its expansion by an arbitrary factor `t` if `t * s ∈ S`. -/
@[to_additive "A difference `r -ₒ s` is equal to its expansion by an
arbitrary translation `t` if `t + s ∈ S`."]
protected theorem expand (r : X) (s : S) (t : R) (hst : t * (s : R) ∈ S) :
    r /ₒ s = t • r /ₒ ⟨t * s, hst⟩ := by
  apply Quotient.sound
  exact ⟨s, s * t, by rw [mul_smul, Submonoid.smul_def], by rw [← mul_assoc]⟩

Expansion Property of Ore Fractions: $r /ₒ s = (t \cdot r) /ₒ (t \cdot s)$ when $t \cdot s \in S$

Informal description

Let $R$ be a monoid and $S$ a left Ore subset of $R$. For any element $r$ in a type $X$ with a multiplicative $R$-action, any denominator $s \in S$, and any element $t \in R$ such that $t \cdot s \in S$, the Ore fraction $r /ₒ s$ is equal to its expansion $(t \cdot r) /ₒ (t \cdot s)$.

OreLocalization.expand' theorem

(r : X) (s s' : S) : r /ₒ s = s' • r /ₒ (s' * s)

Full source

/-- A fraction is equal to its expansion by a factor from `S`. -/
@[to_additive "A difference is equal to its expansion by a summand from `S`."]
protected theorem expand' (r : X) (s s' : S) : r /ₒ s = s' • r /ₒ (s' * s) :=
  OreLocalization.expand r s s' (by norm_cast; apply SetLike.coe_mem)

Expansion Property of Ore Fractions: $r /ₒ s = (s' \cdot r) /ₒ (s' \cdot s)$

Informal description

For any element $r$ in a type $X$ with a multiplicative action of a monoid $R$, and any denominators $s, s'$ in a left Ore set $S \subseteq R$, the Ore fraction $r /ₒ s$ is equal to its expansion $(s' \cdot r) /ₒ (s' \cdot s)$.

OreLocalization.liftExpand definition

 {C : Sort*} (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[S⁻¹] → C

Full source

/-- A function or predicate over `X` and `S` can be lifted to `X[S⁻¹]` if it is invariant
under expansion on the left. -/
@[to_additive "A function or predicate over `X` and `S` can be lifted to the localizaton if it is
invariant under expansion on the left."]
def liftExpand {C : Sort*} (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[S⁻¹] → C :=
  Quotient.lift (fun p : X × S => P p.1 p.2) fun (r₁, s₁) (r₂, s₂) ⟨u, v, hr₂, hs₂⟩ => by
    dsimp at *
    have s₁vS : v * s₁ ∈ S := by
      rw [← hs₂, ← S.coe_mul]
      exact SetLike.coe_mem (u * s₂)
    replace hs₂ : u * s₂ = ⟨_, s₁vS⟩ := by ext; simp [hs₂]
    rw [hP r₁ v s₁ s₁vS, hP r₂ u s₂ (by norm_cast; rwa [hs₂]), ← hr₂]
    simp only [← hs₂]; rfl

Lifting a predicate invariant under left expansion to Ore localization

Informal description

Given a type `C`, a predicate `P : X → S → C`, and a proof `hP` that `P` is invariant under left expansion (i.e., for any `r : X`, `t : R`, `s : S` with `t * s ∈ S`, `P r s = P (t • r) (t * s)`), the function `liftExpand` lifts `P` to a function from the Ore localization `X[S⁻¹]` to `C`. More precisely, `liftExpand` takes an equivalence class `[r /ₒ s]` in `X[S⁻¹]` and returns `P r s`, which is well-defined due to the invariance condition `hP`.

OreLocalization.liftExpand_of theorem

 {C : Sort*} {P : X → S → C} {hP : ∀ (r : X) (t : R) (s : S) (ht : t * s ∈ S), P r s = P (t • r) ⟨t * s, ht⟩} (r : X)
  (s : S) : liftExpand P hP (r /ₒ s) = P r s

Full source

@[to_additive (attr := simp)]
theorem liftExpand_of {C : Sort*} {P : X → S → C}
    {hP : ∀ (r : X) (t : R) (s : S) (ht : t * s ∈ S), P r s = P (t • r) ⟨t * s, ht⟩} (r : X)
    (s : S) : liftExpand P hP (r /ₒ s) = P r s :=
  rfl

Lift of Left Expansion-Invariant Predicate on Ore Localization

Informal description

Let $R$ be a monoid and $S \subseteq R$ a left Ore set. Given a type $C$, a predicate $P : X \to S \to C$, and a proof that $P$ is invariant under left expansion (i.e., for any $r \in X$, $t \in R$, $s \in S$ with $t \cdot s \in S$, we have $P(r, s) = P(t \cdot r, t \cdot s)$), then for any $r \in X$ and $s \in S$, the lift of $P$ to the Ore localization $X[S^{-1}]$ satisfies $\text{liftExpand}\, P\, hP\, (r /_o s) = P\, r\, s$.

OreLocalization.lift₂Expand definition

 {C : Sort*} (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₂⟩) :
  X[S⁻¹] → X[S⁻¹] → C

Full source

/-- A version of `liftExpand` used to simultaneously lift functions with two arguments
in `X[S⁻¹]`. -/
@[to_additive "A version of `liftExpand` used to simultaneously lift functions with two arguments"]
def lift₂Expand {C : Sort*} (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₂⟩) :
    X[S⁻¹] → X[S⁻¹] → C :=
  liftExpand
    (fun r₁ s₁ => liftExpand (P r₁ s₁) fun r₂ t₂ s₂ ht₂ => by
      have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂
      simp [this])
    fun r₁ t₁ s₁ ht₁ => by
    ext x; induction' x with r₂ s₂
    dsimp only
    rw [liftExpand_of, liftExpand_of, hP r₁ t₁ s₁ ht₁ r₂ 1 s₂ (by simp)]; simp

Lifting a binary predicate invariant under left expansion to Ore localization

Informal description

Given a type `C` and a predicate `P : X → S → X → S → C` that is invariant under left expansion (i.e., for any `r₁, r₂ : X`, `t₁, t₂ : R`, `s₁, s₂ : S` with `t₁ * s₁ ∈ S` and `t₂ * s₂ ∈ S`, `P r₁ s₁ r₂ s₂ = P (t₁ • r₁) (t₁ * s₁) (t₂ • r₂) (t₂ * s₂)`), the function `lift₂Expand` lifts `P` to a function from `X[S⁻¹] × X[S⁻¹]` to `C`. More precisely, `lift₂Expand` takes two equivalence classes `[r₁ /ₒ s₁]` and `[r₂ /ₒ s₂]` in `X[S⁻¹]` and returns `P r₁ s₁ r₂ s₂`, which is well-defined due to the invariance condition `hP`.

OreLocalization.lift₂Expand_of theorem

 {C : Sort*} {P : X → S → X → S → C}
  {hP :
    ∀ (r₁ : X) (t₁ : R) (s₁ : S) (ht₁ : t₁ * s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : S) (ht₂ : t₂ * s₂ ∈ S),
      P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * s₂, ht₂⟩}
  (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) : lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂

Full source

@[to_additive (attr := simp)]
theorem lift₂Expand_of {C : Sort*} {P : X → S → X → S → C}
    {hP :
      ∀ (r₁ : X) (t₁ : R) (s₁ : S) (ht₁ : t₁ * s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : S)
        (ht₂ : t₂ * s₂ ∈ S),
        P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * s₂, ht₂⟩}
    (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) : lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂ :=
  rfl

Lift of Left Expansion-Invariant Binary Predate on Ore Localization

Informal description

Let $R$ be a monoid and $S \subseteq R$ a left Ore set. Given a type $C$ and a predicate $P : X \to S \to X \to S \to C$ that is invariant under left expansion (i.e., for any $r_1, r_2 \in X$, $t_1, t_2 \in R$, $s_1, s_2 \in S$ with $t_1 \cdot s_1 \in S$ and $t_2 \cdot s_2 \in S$, we have $P(r_1, s_1, r_2, s_2) = P(t_1 \cdot r_1, t_1 \cdot s_1, t_2 \cdot r_2, t_2 \cdot s_2)$), then for any $r_1, r_2 \in X$ and $s_1, s_2 \in S$, the lift of $P$ to the Ore localization $X[S^{-1}]$ satisfies \[ \text{lift₂Expand}\, P\, hP\, (r_1 /_o s_1)\, (r_2 /_o s_2) = P\, r_1\, s_1\, r_2\, s_2. \]

OreLocalization.smul definition

: R[S⁻¹] → X[S⁻¹] → X[S⁻¹]

Full source

/-- The scalar multiplication on the Ore localization of monoids. -/
@[to_additive (attr := irreducible)
  "the vector addition on the Ore localization of additive monoids."]
protected def smul : R[S⁻¹] → X[S⁻¹] → X[S⁻¹] :=
  liftExpand smul'' fun r₁ r₂ s hs => by
    ext x
    induction' x with x s₂
    show OreLocalization.smul' r₁ s x s₂ = OreLocalization.smul' (r₂ * r₁) ⟨_, hs⟩ x s₂
    rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩
    rw [smul'_char _ _ _ _ _ _ h₁]
    rcases oreCondition (r₂ * r₁) s₂ with ⟨r₂', s₂', h₂⟩
    rw [smul'_char _ _ _ _ _ _ h₂]
    rcases oreCondition (s₂' * r₂) (s₁') with ⟨r₃', s₃', h₃⟩
    have : s₃' * r₂' * s₂ = r₃' * r₁' * s₂ := by
      rw [mul_assoc, ← h₂, ← mul_assoc _ r₂, ← mul_assoc, h₃, mul_assoc, h₁, mul_assoc]
    rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩
    have : (s₄' * r₃') * (s₁' * s) ∈ S := by
      rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
      exact mul_mem (s₄' * s₃' * s₂').2 hs
    rw [OreLocalization.expand' (r₂' • x) _ (s₄' * s₃'), OreLocalization.expand _ _ _ this]
    simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]
    congr 1
    ext; simp only [Submonoid.coe_mul, ← mul_assoc]
    rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc]

Scalar multiplication on Ore localizations

Informal description

The scalar multiplication operation on the Ore localization of a monoid $R$ at a left Ore set $S$ acting on the Ore localization of a type $X$ with a multiplicative action of $R$. Given $[r] \in R[S^{-1}]$ and $[x] \in X[S^{-1}]$, the operation returns $[r \cdot x] \in X[S^{-1}]$, where the multiplication is well-defined via the Ore condition.

OreLocalization.instSMul instance

: SMul R[S⁻¹] X[S⁻¹]

Full source

@[to_additive]
instance : SMul R[S⁻¹] X[S⁻¹] :=
  ⟨OreLocalization.smul⟩

Scalar Multiplication on Ore Localizations

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ has a canonical scalar multiplication operation on the Ore localization $X[S^{-1}]$ of any type $X$ with a multiplicative action of $R$.

OreLocalization.instMul instance

: Mul R[S⁻¹]

Full source

@[to_additive]
instance : Mul R[S⁻¹] :=
  ⟨OreLocalization.smul⟩

Multiplication Operation on Ore Localization

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ is equipped with a multiplication operation defined by $(r_1 /ₒ s_1) * (r_2 /ₒ s_2) = (u \cdot r_1 \cdot r_2) /ₒ (v \cdot s_1 \cdot s_2)$, where $u \in S$ and $v \in R$ are elements satisfying the Ore condition $u \cdot s_2 = v \cdot s_1$.

OreLocalization.oreDiv_smul_oreDiv theorem

 {r₁ : R} {r₂ : X} {s₁ s₂ : S} : (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Full source

@[to_additive]
theorem oreDiv_smul_oreDiv {r₁ : R} {r₂ : X} {s₁ s₂ : S} :
    (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNumoreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) := by
  with_unfolding_all rfl

Scalar Multiplication Formula in Ore Localization: $(r_1 /_o s_1) \cdot (r_2 /_o s_2) = (\text{oreNum}(r_1, s_2) \cdot r_2) /_o (\text{oreDenom}(r_1, s_2) \cdot s_1)$

Informal description

Let $R$ be a monoid with a left Ore set $S$, and let $X$ be a type with a multiplicative action of $R$. For any elements $r_1 \in R$, $r_2 \in X$, and $s_1, s_2 \in S$, the scalar multiplication in the Ore localization satisfies $$(r_1 /_o s_1) \cdot (r_2 /_o s_2) = (\text{oreNum}(r_1, s_2) \cdot r_2) /_o (\text{oreDenom}(r_1, s_2) \cdot s_1),$$ where $\text{oreNum}(r_1, s_2) \in R$ and $\text{oreDenom}(r_1, s_2) \in S$ are elements satisfying the Ore condition for $r_1$ and $s_2$.

OreLocalization.oreDiv_mul_oreDiv theorem

 {r₁ : R} {r₂ : R} {s₁ s₂ : S} : (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Full source

@[to_additive]
theorem oreDiv_mul_oreDiv {r₁ : R} {r₂ : R} {s₁ s₂ : S} :
    (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = oreNumoreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁) := by
  with_unfolding_all rfl

Multiplication Formula for Ore Fractions: $(r_1 /ₒ s_1) * (r_2 /ₒ s_2) = (\text{oreNum}(r_1, s_2) \cdot r_2) /ₒ (\text{oreDenom}(r_1, s_2) \cdot s_1)$

Informal description

For any elements $r_1, r_2$ in a monoid $R$ and any elements $s_1, s_2$ in a left Ore set $S \subseteq R$, the product of the Ore fractions $r_1 /ₒ s_1$ and $r_2 /ₒ s_2$ in the Ore localization $R[S^{-1}]$ is given by $(r_1 /ₒ s_1) * (r_2 /ₒ s_2) = (\text{oreNum}(r_1, s_2) \cdot r_2) /ₒ (\text{oreDenom}(r_1, s_2) \cdot s_1)$, where $\text{oreNum}(r_1, s_2) \in R$ and $\text{oreDenom}(r_1, s_2) \in S$ are elements satisfying the left Ore condition for $r_1$ and $s_2$.

OreLocalization.oreDiv_smul_char theorem

 (r₁ : R) (r₂ : X) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
  (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Full source

/-- A characterization lemma for the scalar multiplication on the Ore localization,
allowing for a choice of Ore numerator and Ore denominator. -/
@[to_additive "A characterization lemma for the vector addition on the Ore localization,
allowing for a choice of Ore minuend and Ore subtrahend."]
theorem oreDiv_smul_char (r₁ : R) (r₂ : X) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
    (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁) := by
  with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Characterization of Scalar Multiplication in Ore Localization

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$, and let $X$ be a type with a multiplicative action of $R$. For any elements $r_1 \in R$, $r_2 \in X$, $s_1, s_2 \in S$, and given $r' \in R$, $s' \in S$ such that $s' \cdot r_1 = r' \cdot s_2$, the scalar multiplication in the Ore localization satisfies \[ (r_1 /_o s_1) \cdot (r_2 /_o s_2) = (r' \cdot r_2) /_o (s' \cdot s_1). \]

OreLocalization.oreDiv_mul_char theorem

 (r₁ r₂ : R) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Full source

/-- A characterization lemma for the multiplication on the Ore localization, allowing for a choice
of Ore numerator and Ore denominator. -/
@[to_additive "A characterization lemma for the addition on the Ore localization,
allowing for a choice of Ore minuend and Ore subtrahend."]
theorem oreDiv_mul_char (r₁ r₂ : R) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
    r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁) := by
  with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Characterization of Multiplication in Ore Localization

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$. For any elements $r_1, r_2 \in R$ and $s_1, s_2 \in S$, if there exist $r' \in R$ and $s' \in S$ such that $s' \cdot r_1 = r' \cdot s_2$, then the product in the Ore localization $R[S^{-1}]$ satisfies: \[ (r_1 /ₒ s_1) \cdot (r_2 /ₒ s_2) = r' \cdot r_2 /ₒ (s' \cdot s_1). \]

OreLocalization.oreDivSMulChar' definition

 (r₁ : R) (r₂ : X) (s₁ s₂ : S) :
  Σ' r' : R, Σ' s' : S, s' * r₁ = r' * s₂ ∧ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Full source

/-- Another characterization lemma for the scalar multiplication on the Ore localizaion delivering
Ore witnesses and conditions bundled in a sigma type. -/
@[to_additive "Another characterization lemma for the vector addition on the
  Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type."]
def oreDivSMulChar' (r₁ : R) (r₂ : X) (s₁ s₂ : S) :
    Σ'r' : R, Σ's' : S, s' * r₁ = r' * s₂ ∧ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁) :=
  ⟨oreNum r₁ s₂, oreDenom r₁ s₂, ore_eq r₁ s₂, oreDiv_smul_oreDiv⟩

Characterization of scalar multiplication in Ore localization via Ore witnesses

Informal description

Given elements $r_1 \in R$, $r_2 \in X$, and denominators $s_1, s_2 \in S$, there exist elements $r' \in R$ and $s' \in S$ such that $s' \cdot r_1 = r' \cdot s_2$ and the scalar multiplication $(r_1 / s_1) \cdot (r_2 / s_2)$ in the Ore localization equals $(r' \cdot r_2) / (s' \cdot s_1)$. Here, $R$ is a monoid, $S$ is a left Ore subset of $R$, and $X$ is a type with a multiplicative action of $R$. The notation $r / s$ represents the Ore division of $r$ by $s$ in the Ore localization $R[S^{-1}]$ or $X[S^{-1}]$.

OreLocalization.oreDivMulChar' definition

 (r₁ r₂ : R) (s₁ s₂ : S) : Σ' r' : R, Σ' s' : S, s' * r₁ = r' * s₂ ∧ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Full source

/-- Another characterization lemma for the multiplication on the Ore localizaion delivering
Ore witnesses and conditions bundled in a sigma type. -/
@[to_additive "Another characterization lemma for the addition on the Ore localizaion delivering
  Ore witnesses and conditions bundled in a sigma type."]
def oreDivMulChar' (r₁ r₂ : R) (s₁ s₂ : S) :
    Σ'r' : R, Σ's' : S, s' * r₁ = r' * s₂ ∧ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁) :=
  ⟨oreNum r₁ s₂, oreDenom r₁ s₂, ore_eq r₁ s₂, oreDiv_mul_oreDiv⟩

Characterization of multiplication in Ore localization via Ore witnesses

Informal description

Given elements $r_1, r_2$ in a monoid $R$ and denominators $s_1, s_2$ in a left Ore set $S \subseteq R$, there exist elements $r' \in R$ and $s' \in S$ such that $s' \cdot r_1 = r' \cdot s_2$ and the product in the Ore localization satisfies: \[ (r_1 /ₒ s_1) \cdot (r_2 /ₒ s_2) = r' \cdot r_2 /ₒ (s' \cdot s_1). \]

OreLocalization.one definition

: R[S⁻¹]

Full source

/-- `1` in the localization, defined as `1 /ₒ 1`. -/
@[to_additive (attr := irreducible) "`0` in the additive localization, defined as `0 -ₒ 0`."]
protected def one : R[S⁻¹] := 1 /ₒ 1

Identity element in Ore localization

Informal description

The multiplicative identity in the Ore localization $R[S^{-1}]$ is defined as the equivalence class of the pair $(1, 1)$ under the Ore equivalence relation, where $1$ is the multiplicative identity of the monoid $R$ and the submonoid $S$.

OreLocalization.instOne instance

: One R[S⁻¹]

Full source

@[to_additive]
instance : One R[S⁻¹] :=
  ⟨OreLocalization.one⟩

Existence of Identity in Ore Localization

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ has a multiplicative identity element, given by the equivalence class of $(1, 1)$ where $1$ is the identity element of $R$.

OreLocalization.one_def theorem

: (1 : R[S⁻¹]) = 1 /ₒ 1

Full source

@[to_additive]
protected theorem one_def : (1 : R[S⁻¹]) = 1 /ₒ 1 := by
  with_unfolding_all rfl

Identity Element in Ore Localization: $1 = 1 /_o 1$

Informal description

In the Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$, the multiplicative identity element is given by the equivalence class of $(1, 1)$, where $1$ is the identity element of $R$. Formally, this is expressed as $1 = 1 /_o 1$, where $/_o$ denotes the Ore division operation.

OreLocalization.instInhabited instance

: Inhabited R[S⁻¹]

Full source

@[to_additive]
instance : Inhabited R[S⁻¹] :=
  ⟨1⟩

Ore Localization is Inhabited

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ is an inhabited type, meaning it contains at least one element.

OreLocalization.div_eq_one' theorem

{r : R} (hr : r ∈ S) : r /ₒ ⟨r, hr⟩ = 1

Full source

@[to_additive (attr := simp)]
protected theorem div_eq_one' {r : R} (hr : r ∈ S) : r /ₒ ⟨r, hr⟩ = 1 := by
  rw [OreLocalization.one_def, oreDiv_eq_iff]
  exact ⟨⟨r, hr⟩, 1, by simp, by simp⟩

Ore Division of Element by Itself Yields Identity: $r /_o r = 1$

Informal description

For any element $r$ in a left Ore set $S$ of a monoid $R$, the Ore division of $r$ by itself (as an element of $S$) equals the multiplicative identity $1$ in the Ore localization $R[S^{-1}]$, i.e., $r /_o r = 1$.

OreLocalization.div_eq_one theorem

{s : S} : (s : R) /ₒ s = 1

Full source

@[to_additive (attr := simp)]
protected theorem div_eq_one {s : S} : (s : R) /ₒ s = 1 :=
  OreLocalization.div_eq_one' _

Ore Division Identity: $s /_o s = 1$

Informal description

For any element $s$ in a left Ore set $S$ of a monoid $R$, the Ore division of $s$ (viewed as an element of $R$) by itself equals the multiplicative identity $1$ in the Ore localization $R[S^{-1}]$, i.e., $s /_o s = 1$.

OreLocalization.one_smul theorem

(x : X[S⁻¹]) : (1 : R[S⁻¹]) • x = x

Full source

@[to_additive]
protected theorem one_smul (x : X[S⁻¹]) : (1 : R[S⁻¹]) • x = x := by
  induction' x with r s
  simp [OreLocalization.one_def, oreDiv_smul_char 1 r 1 s 1 s (by simp)]

Identity Scalar Multiplication in Ore Localization: $1 \cdot x = x$

Informal description

For any element $x$ in the Ore localization $X[S^{-1}]$ of a type $X$ with a multiplicative action of a monoid $R$ at a left Ore set $S$, the scalar multiplication by the multiplicative identity $1 \in R[S^{-1}]$ satisfies $1 \cdot x = x$.

OreLocalization.one_mul theorem

(x : R[S⁻¹]) : 1 * x = x

Full source

@[to_additive]
protected theorem one_mul (x : R[S⁻¹]) : 1 * x = x :=
  OreLocalization.one_smul x

Left Identity Property in Ore Localization: $1 \cdot x = x$

Informal description

For any element $x$ in the Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$, the product of the multiplicative identity $1$ with $x$ equals $x$, i.e., $1 \cdot x = x$.

OreLocalization.mul_one theorem

(x : R[S⁻¹]) : x * 1 = x

Full source

@[to_additive]
protected theorem mul_one (x : R[S⁻¹]) : x * 1 = x := by
  induction' x with r s
  simp [OreLocalization.one_def, oreDiv_mul_char r (1 : R) s (1 : S) r 1 (by simp)]

Right Identity Property in Ore Localization

Informal description

For any element $x$ in the Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$, the product of $x$ with the multiplicative identity $1$ equals $x$, i.e., $x \cdot 1 = x$.

OreLocalization.mul_smul theorem

(x y : R[S⁻¹]) (z : X[S⁻¹]) : (x * y) • z = x • y • z

Full source

@[to_additive]
protected theorem mul_smul (x y : R[S⁻¹]) (z : X[S⁻¹]) : (x * y) • z = x • y • z := by
  -- Porting note: `assoc_rw` was not ported yet
  induction' x with r₁ s₁
  induction' y with r₂ s₂
  induction' z with r₃ s₃
  rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
  rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩; rw [hb']; clear hb'
  rcases oreCondition ra sb with ⟨rc, sc, hc⟩
  rw [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]; swap
  · rw [← mul_assoc _ ra, hc, mul_assoc, hb, ← mul_assoc]
  rw [← mul_assoc, mul_smul]
  symm; apply oreDiv_smul_char
  rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]

Associativity of Scalar Multiplication in Ore Localization

Informal description

For any elements $x, y$ in the Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$, and any element $z$ in the Ore localization $X[S^{-1}]$ of a type $X$ with a multiplicative action of $R$, the scalar multiplication satisfies the associativity property: \[ (x \cdot y) \cdot z = x \cdot (y \cdot z). \]

OreLocalization.mul_assoc theorem

(x y z : R[S⁻¹]) : x * y * z = x * (y * z)

Full source

@[to_additive]
protected theorem mul_assoc (x y z : R[S⁻¹]) : x * y * z = x * (y * z) :=
  OreLocalization.mul_smul x y z

Associativity of Multiplication in Ore Localization

Informal description

For any elements $x, y, z$ in the Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$, the multiplication operation is associative: \[ (x \cdot y) \cdot z = x \cdot (y \cdot z). \]

OreLocalization.npow definition

: ℕ → R[S⁻¹] → R[S⁻¹]

Full source

/-- `npow` of `OreLocalization` -/
@[to_additive (attr := irreducible) "`nsmul` of `AddOreLocalization`"]
protected def npow : ℕ → R[S⁻¹] → R[S⁻¹] := npowRec

Power operation in Ore localization

Informal description

The power operation on the Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ is defined recursively as follows: - For $n = 0$, it returns the multiplicative identity $1$ of $R[S^{-1}]$. - For $n + 1$, it computes the product of the $n$-th power of an element $x \in R[S^{-1}]$ with $x$ itself. This operation extends the usual power operation in the monoid $R$ to its Ore localization.

OreLocalization.instMonoid instance

: Monoid R[S⁻¹]

Full source

@[to_additive]
instance : Monoid R[S⁻¹] where
  one_mul := OreLocalization.one_mul
  mul_one := OreLocalization.mul_one
  mul_assoc := OreLocalization.mul_assoc
  npow := OreLocalization.npow

Monoid Structure on Ore Localization

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ forms a monoid under the multiplication operation defined by $(r_1 /ₒ s_1) \cdot (r_2 /ₒ s_2) = (u \cdot r_1 \cdot r_2) /ₒ (v \cdot s_1 \cdot s_2)$, where $u \in S$ and $v \in R$ satisfy the Ore condition $u \cdot s_2 = v \cdot s_1$. This monoid structure includes an identity element $1 = 1 /ₒ 1$ and satisfies the usual monoid axioms of associativity and identity.

OreLocalization.instMulActionOreLocalization instance

: MulAction R[S⁻¹] X[S⁻¹]

Full source

@[to_additive]
instance instMulActionOreLocalization : MulAction R[S⁻¹] X[S⁻¹] where
  one_smul := OreLocalization.one_smul
  mul_smul := OreLocalization.mul_smul

Multiplicative Action on Ore Localizations

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ acts multiplicatively on the Ore localization $X[S^{-1}]$ of any type $X$ with a multiplicative action of $R$. This action satisfies the usual properties of a multiplicative action, including associativity and identity.

OreLocalization.mul_inv theorem

(s s' : S) : ((s : R) /ₒ s') * ((s' : R) /ₒ s) = 1

Full source

@[to_additive]
protected theorem mul_inv (s s' : S) : ((s : R) /ₒ s') * ((s' : R) /ₒ s) = 1 := by
  simp [oreDiv_mul_char (s : R) s' s' s 1 1 (by simp)]

Inverse Property in Ore Localization: $(s /_o s') \cdot (s' /_o s) = 1$

Informal description

For any elements $s, s'$ in a left Ore set $S$ of a monoid $R$, the product of the Ore divisions $(s /_o s')$ and $(s' /_o s)$ in the Ore localization $R[S^{-1}]$ equals the multiplicative identity $1$. That is, \[ (s /_o s') \cdot (s' /_o s) = 1. \]

OreLocalization.one_div_smul theorem

{r : X} {s t : S} : ((1 : R) /ₒ t) • (r /ₒ s) = r /ₒ (s * t)

Full source

@[to_additive (attr := simp)]
protected theorem one_div_smul {r : X} {s t : S} : ((1 : R) /ₒ t) • (r /ₒ s) = r /ₒ (s * t) := by
  simp [oreDiv_smul_char 1 r t s 1 s (by simp)]

Scalar multiplication by one in Ore localization: $(1 /_o t) \cdot (r /_o s) = r /_o (s \cdot t)$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$, and let $X$ be a type with a multiplicative action of $R$. For any element $r \in X$ and denominators $s, t \in S$, the scalar multiplication in the Ore localization satisfies \[ (1 /_o t) \cdot (r /_o s) = r /_o (s \cdot t). \]

OreLocalization.one_div_mul theorem

{r : R} {s t : S} : (1 /ₒ t) * (r /ₒ s) = r /ₒ (s * t)

Full source

@[to_additive (attr := simp)]
protected theorem one_div_mul {r : R} {s t : S} : (1 /ₒ t) * (r /ₒ s) = r /ₒ (s * t) := by
  simp [oreDiv_mul_char 1 r t s 1 s (by simp)]

Multiplication of Unit Ore Division: $(1 /ₒ t) \cdot (r /ₒ s) = r /ₒ (s \cdot t)$

Informal description

For any element $r$ in a monoid $R$ and any elements $s, t$ in a left Ore set $S \subseteq R$, the product of the Ore division $1 /ₒ t$ and $r /ₒ s$ in the Ore localization $R[S^{-1}]$ equals $r /ₒ (s \cdot t)$. That is, \[ (1 /ₒ t) \cdot (r /ₒ s) = r /ₒ (s \cdot t). \]

OreLocalization.smul_cancel theorem

{r : X} {s t : S} : ((s : R) /ₒ t) • (r /ₒ s) = r /ₒ t

Full source

@[to_additive (attr := simp)]
protected theorem smul_cancel {r : X} {s t : S} : ((s : R) /ₒ t) • (r /ₒ s) = r /ₒ t := by
  simp [oreDiv_smul_char s.1 r t s 1 1 (by simp)]

Cancellation Property for Scalar Multiplication in Ore Localization: $(s /_o t) \cdot (r /_o s) = r /_o t$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$, and let $X$ be a type with a multiplicative action of $R$. For any element $r \in X$ and denominators $s, t \in S$, the scalar multiplication in the Ore localization satisfies \[ (s /_o t) \cdot (r /_o s) = r /_o t. \]

OreLocalization.mul_cancel theorem

{r : R} {s t : S} : ((s : R) /ₒ t) * (r /ₒ s) = r /ₒ t

Full source

@[to_additive (attr := simp)]
protected theorem mul_cancel {r : R} {s t : S} : ((s : R) /ₒ t) * (r /ₒ s) = r /ₒ t := by
  simp [oreDiv_mul_char s.1 r t s 1 1 (by simp)]

Cancellation Property in Ore Localization: $(s /ₒ t) \cdot (r /ₒ s) = r /ₒ t$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$. For any element $r \in R$ and any elements $s, t \in S$, the multiplication in the Ore localization $R[S^{-1}]$ satisfies: \[ (s /ₒ t) \cdot (r /ₒ s) = r /ₒ t. \]

OreLocalization.smul_cancel' theorem

{r₁ : R} {r₂ : X} {s t : S} : ((r₁ * s) /ₒ t) • (r₂ /ₒ s) = (r₁ • r₂) /ₒ t

Full source

@[to_additive (attr := simp)]
protected theorem smul_cancel' {r₁ : R} {r₂ : X} {s t : S} :
    ((r₁ * s) /ₒ t) • (r₂ /ₒ s) = (r₁ • r₂) /ₒ t := by
  simp [oreDiv_smul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

Scalar Multiplication Cancellation in Ore Localization: $(r_1 s /_o t) \cdot (r_2 /_o s) = (r_1 \cdot r_2) /_o t$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$, and let $X$ be a type with a multiplicative action of $R$. For any elements $r_1 \in R$, $r_2 \in X$, and $s, t \in S$, the scalar multiplication in the Ore localization satisfies \[ (r_1 \cdot s /_o t) \cdot (r_2 /_o s) = (r_1 \cdot r_2) /_o t. \]

OreLocalization.mul_cancel' theorem

{r₁ r₂ : R} {s t : S} : ((r₁ * s) /ₒ t) * (r₂ /ₒ s) = (r₁ * r₂) /ₒ t

Full source

@[to_additive (attr := simp)]
protected theorem mul_cancel' {r₁ r₂ : R} {s t : S} :
    ((r₁ * s) /ₒ t) * (r₂ /ₒ s) = (r₁ * r₂) /ₒ t := by
  simp [oreDiv_mul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

Cancellation Property in Ore Localization: $\frac{r_1 s}{t} \cdot \frac{r_2}{s} = \frac{r_1 r_2}{t}$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$. For any elements $r_1, r_2 \in R$ and $s, t \in S$, the following equality holds in the Ore localization $R[S^{-1}]$: \[ \frac{r_1 \cdot s}{t} \cdot \frac{r_2}{s} = \frac{r_1 \cdot r_2}{t}. \]

OreLocalization.smul_div_one theorem

{p : R} {r : X} {s : S} : (p /ₒ s) • (r /ₒ 1) = (p • r) /ₒ s

Full source

@[to_additive (attr := simp)]
theorem smul_div_one {p : R} {r : X} {s : S} : (p /ₒ s) • (r /ₒ 1) = (p • r) /ₒ s := by
  simp [oreDiv_smul_char p r s 1 p 1 (by simp)]

Scalar Multiplication by Unit Denominator in Ore Localization: $(p /_o s) \cdot (r /_o 1) = (p \cdot r) /_o s$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$, and let $X$ be a type with a multiplicative action of $R$. For any elements $p \in R$, $r \in X$, and $s \in S$, the scalar multiplication in the Ore localization satisfies \[ (p /_o s) \cdot (r /_o 1) = (p \cdot r) /_o s. \]

OreLocalization.mul_div_one theorem

{p r : R} {s : S} : (p /ₒ s) * (r /ₒ 1) = (p * r) /ₒ s

Full source

@[to_additive (attr := simp)]
theorem mul_div_one {p r : R} {s : S} : (p /ₒ s) * (r /ₒ 1) = (p * r) /ₒ s := by
  --TODO use coercion r ↦ r /ₒ 1
  simp [oreDiv_mul_char p r s 1 p 1 (by simp)]

Multiplication with Unit Denominator in Ore Localization

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$. For any elements $p, r \in R$ and $s \in S$, the product in the Ore localization $R[S^{-1}]$ satisfies: \[ (p /ₒ s) \cdot (r /ₒ 1) = (p \cdot r) /ₒ s. \]

OreLocalization.numeratorUnit definition

(s : S) : Units R[S⁻¹]

Full source

/-- The fraction `s /ₒ 1` as a unit in `R[S⁻¹]`, where `s : S`. -/
@[to_additive "The difference `s -ₒ 0` as a an additive unit."]
def numeratorUnit (s : S) : Units R[S⁻¹] where
  val := (s : R) /ₒ 1
  inv := (1 : R) /ₒ s
  val_inv := OreLocalization.mul_inv s 1
  inv_val := OreLocalization.mul_inv 1 s

Unit in Ore localization from denominator $ s $

Informal description

For any element $ s $ in the left Ore set $ S $ of a monoid $ R $, the fraction $ s /_o 1 $ is a unit in the Ore localization $ R[S^{-1}] $, with inverse $ 1 /_o s $.

OreLocalization.numeratorHom definition

: R →* R[S⁻¹]

Full source

/-- The multiplicative homomorphism from `R` to `R[S⁻¹]`, mapping `r : R` to the
fraction `r /ₒ 1`. -/
@[to_additive "The additive homomorphism from `R` to `AddOreLocalization R S`,
  mapping `r : R` to the difference `r -ₒ 0`."]
def numeratorHom : R →* R[S⁻¹] where
  toFun r := r /ₒ 1
  map_one' := by with_unfolding_all rfl
  map_mul' _ _ := mul_div_one.symm

Canonical homomorphism to Ore localization

Informal description

The multiplicative homomorphism from a monoid $ R $ to its Ore localization $ R[S^{-1}] $, which maps each element $ r \in R $ to the fraction $ r /ₒ 1 $, where $ 1 $ is the multiplicative identity in the submonoid $ S $. This homomorphism preserves the multiplicative identity and the multiplication operation.

OreLocalization.numeratorHom_apply theorem

{r : R} : numeratorHom r = r /ₒ (1 : S)

Full source

@[to_additive]
theorem numeratorHom_apply {r : R} : numeratorHom r = r /ₒ (1 : S) :=
  rfl

Canonical Homomorphism Maps Element to Fraction with Unit Denominator

Informal description

For any element $r$ in the monoid $R$, the canonical homomorphism $\text{numeratorHom}$ from $R$ to its Ore localization $R[S^{-1}]$ maps $r$ to the fraction $r /ₒ 1$, where $1$ is the multiplicative identity in the submonoid $S$.

OreLocalization.numerator_isUnit theorem

(s : S) : IsUnit (numeratorHom (s : R) : R[S⁻¹])

Full source

@[to_additive]
theorem numerator_isUnit (s : S) : IsUnit (numeratorHom (s : R) : R[S⁻¹]) :=
  ⟨numeratorUnit s, rfl⟩

Units in Ore Localization from Denominator Elements

Informal description

For any element $s$ in the left Ore set $S$ of a monoid $R$, the image of $s$ under the canonical homomorphism to the Ore localization $R[S^{-1}]$ is a unit in $R[S^{-1}]$.

OreLocalization.universalMulHom definition

(hf : ∀ s : S, f s = fS s) : R[S⁻¹] →* T

Full source

/-- The universal lift from a morphism `R →* T`, which maps elements of `S` to units of `T`,
to a morphism `R[S⁻¹] →* T`. -/
@[to_additive "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`."]
def universalMulHom (hf : ∀ s : S, f s = fS s) : R[S⁻¹]R[S⁻¹] →* T where
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
  toFun x :=
    x.liftExpand (fun r s => ((fS s)⁻¹ : Units T) * f r) fun r t s ht => by
      simp only [smul_eq_mul]
      have : (fS ⟨t * s, ht⟩ : T) = f t * fS s := by
        simp only [← hf, MonoidHom.map_mul]
      conv_rhs =>
        rw [MonoidHom.map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]
        rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]
      simp only [one_mul, Units.inv_mul]
  map_one' := by beta_reduce; rw [OreLocalization.one_def, liftExpand_of]; simp
  map_mul' x y := by
    beta_reduce
    induction' x with r₁ s₁
    induction' y with r₂ s₂
    rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
    rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]

Universal homomorphism from Ore localization

Informal description

Given a monoid homomorphism $ f \colon R \to T $ and a function $ fS \colon S \to T^\times $ mapping elements of the left Ore set $ S $ to units of $ T $, such that $ f(s) = fS(s) $ for all $ s \in S $, the universal multiplicative homomorphism $ \text{universalMulHom} $ is the unique monoid homomorphism from the Ore localization $ R[S^{-1}] $ to $ T $ that extends $ f $ and $ fS $. For any $ r \in R $ and $ s \in S $, the homomorphism satisfies: \[ \text{universalMulHom}(r / s) = (fS(s))^{-1} \cdot f(r). \]

OreLocalization.universalMulHom_apply theorem

{r : R} {s : S} : universalMulHom f fS hf (r /ₒ s) = ((fS s)⁻¹ : Units T) * f r

Full source

@[to_additive]
theorem universalMulHom_apply {r : R} {s : S} :
    universalMulHom f fS hf (r /ₒ s) = ((fS s)⁻¹ : Units T) * f r :=
  rfl

Universal Homomorphism Formula for Ore Localization

Informal description

For any element $r \in R$ and any denominator $s \in S$, the universal homomorphism $\text{universalMulHom}$ from the Ore localization $R[S^{-1}]$ to a monoid $T$ satisfies: \[ \text{universalMulHom}(r / s) = (f_S(s))^{-1} \cdot f(r), \] where $f \colon R \to T$ is a monoid homomorphism, $f_S \colon S \to T^\times$ maps elements of $S$ to units of $T$, and $f(s) = f_S(s)$ for all $s \in S$.

OreLocalization.universalMulHom_commutes theorem

{r : R} : universalMulHom f fS hf (numeratorHom r) = f r

Full source

@[to_additive]
theorem universalMulHom_commutes {r : R} : universalMulHom f fS hf (numeratorHom r) = f r := by
  simp [numeratorHom_apply, universalMulHom_apply]

Commutativity of Universal Homomorphism with Numerator Map in Ore Localization

Informal description

For any monoid homomorphism $f \colon R \to T$ and function $fS \colon S \to T^\times$ satisfying $f(s) = fS(s)$ for all $s \in S$, the universal homomorphism $\text{universalMulHom}\, f\, fS\, hf$ from the Ore localization $R[S^{-1}]$ to $T$ commutes with the numerator homomorphism, i.e., for any $r \in R$, \[ \text{universalMulHom}\, f\, fS\, hf\, (r /ₒ 1) = f(r). \]

OreLocalization.universalMulHom_unique theorem

(φ : R[S⁻¹] →* T) (huniv : ∀ r : R, φ (numeratorHom r) = f r) : φ = universalMulHom f fS hf

Full source

/-- The universal morphism `universalMulHom` is unique. -/
@[to_additive "The universal morphism `universalAddHom` is unique."]
theorem universalMulHom_unique (φ : R[S⁻¹]R[S⁻¹] →* T) (huniv : ∀ r : R, φ (numeratorHom r) = f r) :
    φ = universalMulHom f fS hf := by
  ext x; induction' x with r s
  rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]

Uniqueness of the Universal Homomorphism from Ore Localization

Informal description

Let $R$ be a monoid with a left Ore set $S$, and let $T$ be another monoid. Given a monoid homomorphism $f \colon R \to T$ and a function $f_S \colon S \to T^\times$ such that $f(s) = f_S(s)$ for all $s \in S$, the universal homomorphism $\text{universalMulHom}\, f\, f_S\, hf$ from the Ore localization $R[S^{-1}]$ to $T$ is the unique monoid homomorphism $\varphi \colon R[S^{-1}] \to T$ satisfying $\varphi(r /ₒ 1) = f(r)$ for all $r \in R$.

OreLocalization.hsmul definition

(c : R) : X[S⁻¹] → X[S⁻¹]

Full source

/-- Scalar multiplication in a monoid localization. -/
@[to_additive (attr := irreducible) "Vector addition in an additive monoid localization."]
protected def hsmul (c : R) :
    X[S⁻¹] → X[S⁻¹] :=
  liftExpand (fun m s ↦ oreNumoreNum (c • 1) s • m /ₒ oreDenom (c • 1) s) (fun r t s ht ↦ by
    dsimp only
    rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand])

Scalar multiplication in Ore localization

Informal description

The scalar multiplication operation in the Ore localization of a monoid action, defined as follows: for any element $c \in R$, the operation $hsmul(c)$ maps an element $[m /ₒ s]$ in the Ore localization $X[S^{-1}]$ to $[ (oreNum(c \cdot 1) s) \cdot m /ₒ oreDenom(c \cdot 1) s ]$, where $oreNum$ and $oreDenom$ are functions that extract the numerator and denominator from the Ore condition. This operation is well-defined due to the invariance under left expansion property of the Ore localization.

OreLocalization.instSMulOfIsScalarTower instance

[SMul R X] [SMul R M] [IsScalarTower R M X] [IsScalarTower R M M] : SMul R (X[S⁻¹])

Full source

@[to_additive (attr := nolint unusedArguments)]
instance [SMul R X] [SMul R M] [IsScalarTower R M X] [IsScalarTower R M M] : SMul R (X[S⁻¹]) where
  smul := OreLocalization.hsmul

Scalar Multiplication on Ore Localization via Scalar Tower

Informal description

Given a monoid $R$ acting on a type $X$ and a submonoid $S$ of $R$ satisfying the left Ore condition, the Ore localization $X[S^{-1}]$ inherits a scalar multiplication operation from $R$. This operation is well-defined when $R$ acts compatibly on both $M$ and $X$ through scalar tower structures.

OreLocalization.smul_oreDiv theorem

(r : R) (x : X) (s : S) : r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

Full source

@[to_additive]
theorem smul_oreDiv (r : R) (x : X) (s : S) :
    r • (x /ₒ s) = oreNumoreNum (r • 1) s • x /ₒ oreDenom (r • 1) s := by with_unfolding_all rfl

Scalar multiplication formula for Ore fractions: $r \cdot (x /ₒ s) = (u \cdot r) \cdot x /ₒ (u \cdot s)$

Informal description

Let $R$ be a monoid acting on a type $X$, and let $S$ be a left Ore submonoid of $R$. For any $r \in R$, $x \in X$, and $s \in S$, the scalar multiplication of $r$ with the Ore fraction $x /ₒ s$ is given by: \[ r \cdot (x /ₒ s) = (u \cdot r) \cdot x /ₒ (u \cdot s) \] where $u \in S$ and $v \in R$ are elements satisfying the left Ore condition for $r$ and $s$ (i.e., $u \cdot r = v \cdot s$).

OreLocalization.oreDiv_one_smul theorem

(r : M) (x : X[S⁻¹]) : (r /ₒ (1 : S)) • x = r • x

Full source

@[to_additive (attr := simp)]
theorem oreDiv_one_smul (r : M) (x : X[S⁻¹]) : (r /ₒ (1 : S)) • x = r • x := by
  induction' x using OreLocalization.ind with r' s
  rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]

Scalar multiplication identity: $(r /ₒ 1) \cdot x = r \cdot x$ in Ore localization

Informal description

For any element $r$ in a monoid $M$ and any element $x$ in the Ore localization $X[S^{-1}]$, the scalar multiplication of $x$ by the Ore fraction $r /ₒ 1$ (where $1$ is the multiplicative identity in the submonoid $S$) is equal to the scalar multiplication of $x$ by $r$ itself, i.e., $(r /ₒ 1) \cdot x = r \cdot x$.

OreLocalization.smul_one_smul theorem

(r : R) (x : X[S⁻¹]) : (r • 1 : M) • x = r • x

Full source

@[to_additive]
theorem smul_one_smul (r : R) (x : X[S⁻¹]) : (r • 1 : M) • x = r • x := by
  induction' x using OreLocalization.ind with r' s
  simp only [smul_oreDiv, smul_eq_mul, mul_one]

Scalar Multiplication Identity in Ore Localization: $(r \cdot 1) \cdot x = r \cdot x$

Informal description

For any element $r$ in a monoid $R$ and any element $x$ in the Ore localization $X[S^{-1}]$, the scalar multiplication of $x$ by $r \cdot 1$ (where $1$ is the multiplicative identity in $R$) is equal to the scalar multiplication of $x$ by $r$ itself, i.e., $(r \cdot 1) \cdot x = r \cdot x$.

OreLocalization.smul_one_oreDiv_one_smul theorem

(r : R) (x : X[S⁻¹]) : ((r • 1 : M) /ₒ (1 : S)) • x = r • x

Full source

@[to_additive]
theorem smul_one_oreDiv_one_smul (r : R) (x : X[S⁻¹]) :
    ((r • 1 : M) /ₒ (1 : S)) • x = r • x := by
  rw [oreDiv_one_smul, smul_one_smul]

Scalar Multiplication Identity via Ore Fraction: $((r \cdot 1) /ₒ 1) \cdot x = r \cdot x$

Informal description

For any element $r$ in a monoid $R$ and any element $x$ in the Ore localization $X[S^{-1}]$, the scalar multiplication of $x$ by the Ore fraction $(r \cdot 1) /ₒ 1$ (where $1$ is the multiplicative identity in the submonoid $S$) is equal to the scalar multiplication of $x$ by $r$ itself, i.e., $((r \cdot 1) /ₒ 1) \cdot x = r \cdot x$.

OreLocalization.instIsScalarTower instance

: IsScalarTower R R' X[S⁻¹]

Full source

@[to_additive]
instance : IsScalarTower R R' X[S⁻¹] where
  smul_assoc r m x := by
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul,
      ← mul_smul, mul_div_one]
    simp only [smul_eq_mul, mul_one, smul_mul_assoc, smul_assoc, one_mul]

Scalar Tower Property for Ore Localizations

Informal description

For a monoid $R$ acting on a type $X$ with a left Ore set $S \subseteq R$, and another monoid $R'$ acting on $R$ and $X$ compatibly, the Ore localization $X[S^{-1}]$ forms a scalar tower structure. This means that for any $r \in R$, $r' \in R'$, and $x \in X[S^{-1}]$, the scalar multiplications satisfy $(r' \cdot r) \cdot x = r' \cdot (r \cdot x)$.

OreLocalization.instSMulCommClass instance

[SMulCommClass R R' M] : SMulCommClass R R' X[S⁻¹]

Full source

@[to_additive]
instance [SMulCommClass R R' M] : SMulCommClass R R' X[S⁻¹] where
  smul_comm r m x := by
    rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]

Commuting Scalar Actions on Ore Localizations

Informal description

For any monoids $R$ and $R'$ acting on a monoid $M$ with commuting scalar multiplications (i.e., $r \cdot (r' \cdot m) = r' \cdot (r \cdot m)$ for all $r \in R$, $r' \in R'$, $m \in M$), the Ore localization $X[S^{-1}]$ of any type $X$ with a multiplicative action of $R$ inherits this commuting scalar multiplication property. That is, the scalar actions of $R$ and $R'$ on $X[S^{-1}]$ commute.

OreLocalization.instIsScalarTower_1 instance

: IsScalarTower R M[S⁻¹] X[S⁻¹]

Full source

@[to_additive]
instance : IsScalarTower R M[S⁻¹] X[S⁻¹] where
  smul_assoc r m x := by
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]

Scalar Tower Property for Ore Localizations

Informal description

For a monoid $R$ with a left Ore set $S$, the Ore localization $R[S^{-1}]$ acts on the Ore localization $X[S^{-1}]$ of any type $X$ with a multiplicative action of $R$, and this action forms a scalar tower with the action of $R$ on $M[S^{-1}]$ and $X[S^{-1}]$. Specifically, for any $r \in R$, $m \in M[S^{-1}]$, and $x \in X[S^{-1}]$, we have $r \cdot (m \cdot x) = (r \cdot m) \cdot x$.

OreLocalization.instSMulCommClass_1 instance

[SMulCommClass R M M] : SMulCommClass R M[S⁻¹] X[S⁻¹]

Full source

@[to_additive]
instance [SMulCommClass R M M] : SMulCommClass R M[S⁻¹] X[S⁻¹] where
  smul_comm r x y := by
    induction' x using OreLocalization.ind with r₁ s₁
    induction' y using OreLocalization.ind with r₂ s₂
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, smul_smul, smul_smul,
      mul_div_one, oreDiv_mul_char _ _ _ _ (r • 1) s₁ (by simp), mul_one]
    simp

Commuting Scalar Actions on Ore Localizations

Informal description

For any monoid $R$ with a left Ore set $S \subseteq R$ and a type $X$ with a multiplicative action of $R$, if $R$ and $M$ have commuting scalar multiplications (i.e., $r \cdot (m \cdot x) = m \cdot (r \cdot x)$ for all $r \in R$, $m \in M$, $x \in X$), then the scalar multiplications of $R$ and $M[S^{-1}]$ on $X[S^{-1}]$ also commute.

OreLocalization.instIsCentralScalar instance

 [SMul Rᵐᵒᵖ M] [SMul Rᵐᵒᵖ X] [IsScalarTower Rᵐᵒᵖ M M] [IsScalarTower Rᵐᵒᵖ M X] [IsCentralScalar R M] :
  IsCentralScalar R X[S⁻¹]

Full source

@[to_additive]
instance [SMul Rᵐᵒᵖ M] [SMul Rᵐᵒᵖ X] [IsScalarTower Rᵐᵒᵖ M M] [IsScalarTower Rᵐᵒᵖ M X]
  [IsCentralScalar R M] : IsCentralScalar R X[S⁻¹] where
  op_smul_eq_smul r x := by
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_smul]

Central Scalar Action on Ore Localization via Scalar Tower

Informal description

For any monoid $R$ with a multiplicative action on a monoid $M$ and a type $X$, where $R$ acts compatibly on $M$ and $X$ through scalar tower structures, and given that $R$ has a central scalar action on $M$, the Ore localization $X[S^{-1}]$ inherits a central scalar action from $R$. This means that for any $r \in R$ and $x \in X[S^{-1}]$, the action of $r$ on $x$ is central, i.e., it commutes with the Ore localization structure.

OreLocalization.instMulActionOfIsScalarTower instance

{R} [Monoid R] [MulAction R M] [IsScalarTower R M M] [MulAction R X] [IsScalarTower R M X] : MulAction R X[S⁻¹]

Full source

@[to_additive]
instance {R} [Monoid R] [MulAction R M] [IsScalarTower R M M]
    [MulAction R X] [IsScalarTower R M X] : MulAction R X[S⁻¹] where
  one_smul := OreLocalization.ind fun x s ↦ by
    rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, one_smul]
  mul_smul s₁ s₂ x := by rw [← smul_eq_mul, smul_assoc]

Multiplicative Action on Ore Localization via Scalar Tower

Informal description

For any monoid $R$ with a multiplicative action on a monoid $M$ and a type $X$, where $R$ acts compatibly on $M$ and $X$ through scalar tower structures, the Ore localization $X[S^{-1}]$ inherits a multiplicative action from $R$.

OreLocalization.smul_oreDiv_one theorem

(r : R) (x : X) : r • (x /ₒ (1 : S)) = (r • x) /ₒ (1 : S)

Full source

@[to_additive]
theorem smul_oreDiv_one (r : R) (x : X) : r • (x /ₒ (1 : S)) = (r • x) /ₒ (1 : S) := by
  rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, one_smul]

Scalar Multiplication of Ore Fraction by Unit Denominator: $r \cdot (x /_o 1) = (r \cdot x) /_o 1$

Informal description

For any element $r$ in a monoid $R$ and any element $x$ in a type $X$ with a multiplicative action of $R$, the scalar multiplication of the Ore fraction $x /_o 1$ (where $1$ is the multiplicative identity in the submonoid $S$) by $r$ is equal to the Ore fraction $(r \cdot x) /_o 1$, i.e., \[ r \cdot (x /_o 1) = (r \cdot x) /_o 1. \]

OreLocalization.oreDiv_mul_oreDiv_comm theorem

{r₁ r₂ : R} {s₁ s₂ : S} : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)

Full source

@[to_additive]
theorem oreDiv_mul_oreDiv_comm {r₁ r₂ : R} {s₁ s₂ : S} :
    r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂) := by
  rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]), mul_comm s₂]

Commutativity of Multiplication in Ore Localization: $(r_1 /ₒ s_1) \cdot (r_2 /ₒ s_2) = (r_1 r_2) /ₒ (s_1 s_2)$

Informal description

Let $R$ be a monoid with a left Ore set $S \subseteq R$. For any elements $r_1, r_2 \in R$ and $s_1, s_2 \in S$, the multiplication in the Ore localization $R[S^{-1}]$ satisfies: \[ (r_1 /ₒ s_1) \cdot (r_2 /ₒ s_2) = (r_1 \cdot r_2) /ₒ (s_1 \cdot s_2). \]

OreLocalization.instCommMonoid instance

: CommMonoid R[S⁻¹]

Full source

@[to_additive]
instance : CommMonoid R[S⁻¹] where
  mul_comm := fun x y => by
    induction' x with r₁ s₁
    induction' y with r₂ s₂
    rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]

Commutative Monoid Structure on Ore Localization

Informal description

The Ore localization $R[S^{-1}]$ of a monoid $R$ at a left Ore set $S$ forms a commutative monoid under the multiplication operation defined by $(r_1 /ₒ s_1) \cdot (r_2 /ₒ s_2) = (r_1 \cdot r_2) /ₒ (s_1 \cdot s_2)$. This monoid structure includes an identity element $1 = 1 /ₒ 1$ and satisfies the usual monoid axioms of associativity and identity, with the additional property that the multiplication is commutative.

OreLocalization.zero definition

: X[S⁻¹]

Full source

/-- `0` in the localization, defined as `0 /ₒ 1`. -/
@[irreducible]
protected def zero : X[S⁻¹] := 0 /ₒ 1

Zero element in Ore localization

Informal description

The zero element in the Ore localization $X[S^{-1}]$ is defined as the equivalence class of the pair $(0, 1)$, where $0$ is the additive identity in $X$ and $1$ is the multiplicative identity in the left Ore set $S$.

OreLocalization.instZero instance

: Zero X[S⁻¹]

Full source

instance : Zero X[S⁻¹] :=
  ⟨OreLocalization.zero⟩

Zero Element in Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a type $X$ with a multiplicative action of a monoid $R$ at a left Ore set $S$ is equipped with a zero element.

OreLocalization.zero_def theorem

: (0 : X[S⁻¹]) = 0 /ₒ 1

Full source

protected theorem zero_def : (0 : X[S⁻¹]) = 0 /ₒ 1 := by
  with_unfolding_all rfl

Zero Element in Ore Localization as $0 = 0 /ₒ 1$

Informal description

In the Ore localization $X[S^{-1}]$ of a type $X$ with a multiplicative action of a monoid $R$ at a left Ore set $S$, the zero element is given by the Ore division of the additive identity $0 \in X$ by the multiplicative identity $1 \in S$, i.e., $0 = 0 /ₒ 1$.

Mathlib.GroupTheory.OreLocalization.Basic

Notations

References

Tags