Mathlib.RingTheory.OreLocalization.Basic

OreLocalization.zero_oreDiv' theorem

(s : S) : (0 : R) /ₒ s = 0

Full source

@[simp]
theorem zero_oreDiv' (s : S) : (0 : R) /ₒ s = 0 := by
  rw [OreLocalization.zero_def, oreDiv_eq_iff]
  exact ⟨s, 1, by simp [Submonoid.smul_def]⟩

Ore Localization of Zero is Zero

Informal description

For any element $s$ in the left Ore set $S$, the Ore localization of zero by $s$ equals zero, i.e., $0 /_o s = 0$.

OreLocalization.instMonoidWithZero instance

: MonoidWithZero R[S⁻¹]

Full source

instance : MonoidWithZero R[S⁻¹] where
  zero_mul x := by
    induction' x using OreLocalization.ind with r s
    rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]
  mul_zero x := by
    induction' x using OreLocalization.ind with r s
    rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']

Monoid with Zero Structure on Ore Localization

Informal description

The Ore localization $R[S^{-1}]$ of a ring $R$ with respect to a left Ore set $S$ has a canonical monoid with zero structure.

OreLocalization.instCommMonoidWithZero instance

: CommMonoidWithZero R[S⁻¹]

Full source

instance : CommMonoidWithZero R[S⁻¹] where
  __ := inferInstanceAs (MonoidWithZero R[S⁻¹])
  __ := inferInstanceAs (CommMonoid R[S⁻¹])

Commutative Monoid with Zero Structure on Ore Localization

Informal description

The Ore localization $R[S^{-1}]$ of a ring $R$ with respect to a left Ore set $S$ has a canonical commutative monoid with zero structure.

OreLocalization.instAdd instance

: Add X[S⁻¹]

Full source

instance : Add X[S⁻¹] :=
  ⟨add⟩

Addition on Ore Localization

Informal description

The localization $X[S^{-1}]$ of a ring $X$ over a left Ore set $S$ has a canonical addition operation.

OreLocalization.oreDiv_add_oreDiv theorem

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

Full source

theorem oreDiv_add_oreDiv {r r' : X} {s s' : S} :
    r /ₒ s + r' /ₒ s' =
      (oreDenom (s : R) s' • r + oreNum (s : R) s' • r') /ₒ (oreDenom (s : R) s' * s) := by
  with_unfolding_all rfl

Addition Formula for Ore Localization

Informal description

Let $X$ be a ring with a left Ore set $S$, and let $r, r' \in X$ and $s, s' \in S$. Then the sum of the Ore fractions $r/s$ and $r'/s'$ in the localization $X[S^{-1}]$ is given by \[ \frac{r}{s} + \frac{r'}{s'} = \frac{d(s, s') \cdot r + n(s, s') \cdot r'}{d(s, s') \cdot s}, \] where $n(s, s')$ and $d(s, s')$ are the Ore numerator and denominator respectively, satisfying the Ore condition for $s$ and $s'$.

OreLocalization.oreDiv_add_char' theorem

 {r r' : X} (s s' : S) (rb : R) (sb : R) (h : sb * s = rb * s') (h' : sb * s ∈ S) :
  r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * s, h'⟩

Full source

theorem oreDiv_add_char' {r r' : X} (s s' : S) (rb : R) (sb : R)
    (h : sb * s = rb * s') (h' : sb * s ∈ S) :
    r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * s, h'⟩ := by
  with_unfolding_all exact add''_char r s r' s' rb sb h h'

Addition Formula for Ore Localization with Characteristic Condition

Informal description

Let $X$ be a ring with a left Ore set $S$, and let $r, r' \in X$ and $s, s' \in S$. Suppose there exist elements $r_b \in X$ and $s_b \in X$ such that $s_b s = r_b s'$ and $s_b s \in S$. Then the sum of the fractions $r/s$ and $r'/s'$ in the Ore localization $X[S^{-1}]$ is given by: \[ \frac{r}{s} + \frac{r'}{s'} = \frac{s_b \cdot r + r_b \cdot r'}{s_b s}. \]

OreLocalization.oreDiv_add_char theorem

 {r r' : X} (s s' : S) (rb : R) (sb : S) (h : sb * s = rb * s') : r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s)

Full source

/-- A characterization of the addition on the Ore localizaion, allowing for arbitrary Ore
numerator and Ore denominator. -/
theorem oreDiv_add_char {r r' : X} (s s' : S) (rb : R) (sb : S) (h : sb * s = rb * s') :
    r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s) :=
  oreDiv_add_char' s s' rb sb h (sb * s).2

Addition Formula for Ore Localization with Ore Condition

Informal description

Let $X$ be a ring with a left Ore set $S$, and let $r, r' \in X$ and $s, s' \in S$. Suppose there exist elements $r_b \in X$ and $s_b \in S$ such that $s_b \cdot s = r_b \cdot s'$. Then the sum of the fractions $r/s$ and $r'/s'$ in the Ore localization $X[S^{-1}]$ is given by: \[ \frac{r}{s} + \frac{r'}{s'} = \frac{s_b \cdot r + r_b \cdot r'}{s_b \cdot s}. \]

OreLocalization.oreDivAddChar' definition

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

Full source

/-- Another characterization of the addition on the Ore localization, bundling up all witnesses
and conditions into a sigma type. -/
def oreDivAddChar' (r r' : X) (s s' : S) :
    Σ'r'' : R,
      Σ's'' : S, s'' * s = r'' * s' ∧ r /ₒ s + r' /ₒ s' = (s'' • r + r'' • r') /ₒ (s'' * s) :=
  ⟨oreNum (s : R) s', oreDenom (s : R) s', ore_eq (s : R) s', oreDiv_add_oreDiv⟩

Characterization of Addition in Ore Localization

Informal description

For any elements $r, r'$ in a ring $X$ and any elements $s, s'$ in a left Ore set $S$, there exist elements $r'' \in X$ and $s'' \in S$ such that $s'' \cdot s = r'' \cdot s'$ and the sum of the Ore fractions $r/s + r'/s'$ equals $(s'' \cdot r + r'' \cdot r') / (s'' \cdot s)$. This provides a bundled characterization of addition in the Ore localization.

OreLocalization.add_oreDiv theorem

{r r' : X} {s : S} : r /ₒ s + r' /ₒ s = (r + r') /ₒ s

Full source

@[simp]
theorem add_oreDiv {r r' : X} {s : S} : r /ₒ s + r' /ₒ s = (r + r') /ₒ s := by
  simp [oreDiv_add_char s s 1 1 (by simp)]

Addition of Ore Fractions with Common Denominator

Informal description

For any elements $r, r'$ in a ring $X$ and any element $s$ in a left Ore set $S$, the sum of the Ore fractions $r/s$ and $r'/s$ in the Ore localization $X[S^{-1}]$ is equal to $(r + r')/s$, i.e., \[ \frac{r}{s} + \frac{r'}{s} = \frac{r + r'}{s}. \]

OreLocalization.add_assoc theorem

(x y z : X[S⁻¹]) : x + y + z = x + (y + z)

Full source

protected theorem add_assoc (x y z : X[S⁻¹]) : x + y + z = x + (y + z) := by
  induction' x with r₁ s₁
  induction' y with r₂ s₂
  induction' z with r₃ s₃
  rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
  rcases oreDivAddChar' (sa • r₁ + ra • r₂) r₃ (sa * s₁) s₃ with ⟨rc, sc, hc, q⟩; rw [q]; clear q
  simp only [smul_add, mul_assoc, add_assoc]
  simp_rw [← add_oreDiv, ← OreLocalization.expand']
  congr 2
  · rw [OreLocalization.expand r₂ s₂ ra (ha.symm ▸ (sa * s₁).2)]; congr; ext; exact ha
  · rw [OreLocalization.expand r₃ s₃ rc (hc.symm ▸ (sc * (sa * s₁)).2)]; congr; ext; exact hc

Associativity of Addition in Ore Localization

Informal description

For any elements $x, y, z$ in the Ore localization $X[S^{-1}]$ of a ring $X$ over a left Ore set $S$, the addition operation is associative, i.e., $(x + y) + z = x + (y + z)$.

OreLocalization.zero_oreDiv theorem

(s : S) : (0 : X) /ₒ s = 0

Full source

@[simp]
theorem zero_oreDiv (s : S) : (0 : X) /ₒ s = 0 := by
  rw [OreLocalization.zero_def, oreDiv_eq_iff]
  exact ⟨s, 1, by simp⟩

Ore Localization of Zero is Zero

Informal description

For any element $s$ in the left Ore set $S$, the Ore localization of the zero element $0 \in X$ by $s$ equals zero, i.e., $0 /_o s = 0$.

OreLocalization.zero_add theorem

(x : X[S⁻¹]) : 0 + x = x

Full source

protected theorem zero_add (x : X[S⁻¹]) : 0 + x = x := by
  induction x
  rw [← zero_oreDiv, add_oreDiv]; simp

Left Additive Identity in Ore Localization

Informal description

For any element $x$ in the Ore localization $X[S^{-1}]$ of a ring $X$ over a left Ore set $S$, the sum of the zero element and $x$ is equal to $x$, i.e., $0 + x = x$.

OreLocalization.add_zero theorem

(x : X[S⁻¹]) : x + 0 = x

Full source

protected theorem add_zero (x : X[S⁻¹]) : x + 0 = x := by
  induction x
  rw [← zero_oreDiv, add_oreDiv]; simp

Right Additive Identity in Ore Localization

Informal description

For any element $x$ in the Ore localization $X[S^{-1}]$ of a ring $X$ over a left Ore set $S$, the sum of $x$ and the zero element is equal to $x$, i.e., $x + 0 = x$.

OreLocalization.instAddMonoid instance

: AddMonoid X[S⁻¹]

Full source

instance : AddMonoid X[S⁻¹] where
    add_assoc := OreLocalization.add_assoc
    zero_add := OreLocalization.zero_add
    add_zero := OreLocalization.add_zero
    nsmul := nsmul
    nsmul_zero _ := by with_unfolding_all rfl
    nsmul_succ _ _ := by with_unfolding_all rfl

Additive Monoid Structure on Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a ring $X$ over a left Ore set $S$ has a canonical additive monoid structure.

OreLocalization.smul_zero theorem

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

Full source

protected theorem smul_zero (x : R[S⁻¹]) : x • (0 : X[S⁻¹]) = 0 := by
  induction' x with r s
  rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]

Scalar Multiplication by Zero in Ore Localization

Informal description

For any element $x$ in the Ore localization $R[S^{-1}]$ of a ring $R$ with respect to a left Ore set $S$, the scalar multiplication of $x$ with the zero element in the Ore localization $X[S^{-1}]$ of a module $X$ is equal to zero, i.e., $x \cdot 0 = 0$.

OreLocalization.smul_add theorem

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

Full source

protected theorem smul_add (z : R[S⁻¹]) (x y : X[S⁻¹]) :
    z • (x + y) = z • x + z • y := by
  induction' x with r₁ s₁
  induction' y with r₂ s₂
  induction' z with r₃ s₃
  rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'; norm_cast at ha
  rw [OreLocalization.expand' r₁ s₁ sa]
  rw [OreLocalization.expand r₂ s₂ ra (by rw [← ha]; apply SetLike.coe_mem)]
  rw [← Subtype.coe_eq_of_eq_mk ha]
  repeat rw [oreDiv_smul_oreDiv]
  simp only [smul_add, add_oreDiv]

Distributivity of Scalar Multiplication over Addition in Ore Localization

Informal description

For any element $z$ in the Ore localization $R[S^{-1}]$ and any elements $x, y$ in the Ore localization $X[S^{-1}]$, the scalar multiplication of $z$ with the sum $x + y$ is equal to the sum of the scalar multiplications $z \cdot x + z \cdot y$, i.e., \[ z \cdot (x + y) = z \cdot x + z \cdot y. \]

OreLocalization.instDistribMulAction instance

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

Full source

instance : DistribMulAction R[S⁻¹] X[S⁻¹] where
  smul_zero := OreLocalization.smul_zero
  smul_add := OreLocalization.smul_add

Distributive Multiplicative Action on Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a module $X$ over a ring $R$ with respect to a left Ore set $S$ has a canonical distributive multiplicative action structure induced by the Ore localization $R[S^{-1}]$ of $R$.

OreLocalization.instDistribMulActionOfIsScalarTower instance

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

Full source

instance {R₀} [Monoid R₀] [MulAction R₀ X] [MulAction R₀ R]
    [IsScalarTower R₀ R X] [IsScalarTower R₀ R R] :
    DistribMulAction R₀ X[S⁻¹] where
  smul_zero _ := by rw [← smul_one_oreDiv_one_smul, smul_zero]
  smul_add _ _ _ := by simp only [← smul_one_oreDiv_one_smul, smul_add]

Distributive Multiplicative Action on Ore Localization via Scalar Tower

Informal description

Given a monoid $R_0$ acting on a ring $X$ and on another ring $R$, with compatible scalar tower structures $R_0 \to R \to X$ and $R_0 \to R \to R$, the Ore localization $X[S^{-1}]$ inherits a distributive multiplicative action from $R_0$.

OreLocalization.add_comm theorem

(x y : X[S⁻¹]) : x + y = y + x

Full source

protected theorem add_comm (x y : X[S⁻¹]) : x + y = y + x := by
  induction' x with r s
  induction' y with r' s'
  rcases oreDivAddChar' r r' s s' with ⟨ra, sa, ha, ha'⟩
  rw [ha', oreDiv_add_char' s' s _ _ ha.symm (ha ▸ (sa * s).2), add_comm]
  congr; ext; exact ha

Commutativity of Addition in Ore Localization

Informal description

For any two elements $x$ and $y$ in the Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$, the addition operation is commutative, i.e., $x + y = y + x$.

OreLocalization.instAddCommMonoidOreLocalization instance

: AddCommMonoid X[S⁻¹]

Full source

instance instAddCommMonoidOreLocalization : AddCommMonoid X[S⁻¹] where
  add_comm := OreLocalization.add_comm

Additive Commutative Monoid Structure on Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$ has a canonical additive commutative monoid structure.

OreLocalization.neg definition

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

Full source

/-- Negation on the Ore localization is defined via negation on the numerator. -/
@[irreducible]
protected def neg : X[S⁻¹] → X[S⁻¹] :=
  liftExpand (fun (r : X) (s : S) => -r /ₒ s) fun r t s ht => by
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
    beta_reduce
    rw [← smul_neg, ← OreLocalization.expand]

Negation in Ore localization

Informal description

The negation operation on the Ore localization of a ring $ X $ with respect to a left Ore set $ S $ is defined by negating the numerator. Specifically, for any element $ r \in X $ and $ s \in S $, the negation of the fraction $ r /_o s $ is given by $ -r /_o s $.

OreLocalization.instNegOreLocalization instance

: Neg X[S⁻¹]

Full source

instance instNegOreLocalization : Neg X[S⁻¹] :=
  ⟨OreLocalization.neg⟩

Negation in Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$ is equipped with a negation operation, defined by negating the numerator of each fraction.

OreLocalization.neg_def theorem

(r : X) (s : S) : -(r /ₒ s) = -r /ₒ s

Full source

@[simp]
protected theorem neg_def (r : X) (s : S) : -(r /ₒ s) = -r /ₒ s := by
  with_unfolding_all rfl

Negation of Fractions in Ore Localization: $-(r /_o s) = -r /_o s$

Informal description

For any element $r$ in a ring $X$ and any element $s$ in a left Ore set $S$, the negation of the fraction $r /_o s$ in the Ore localization $X[S^{-1}]$ is equal to the fraction $-r /_o s$.

OreLocalization.neg_add_cancel theorem

(x : X[S⁻¹]) : -x + x = 0

Full source

protected theorem neg_add_cancel (x : X[S⁻¹]) : -x + x = 0 := by
  induction' x with r s; simp

Additive Inverse Property in Ore Localization: $-x + x = 0$

Informal description

For any element $x$ in the Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$, the sum of $-x$ and $x$ equals zero, i.e., $-x + x = 0$.

OreLocalization.zsmul definition

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

Full source

/-- `zsmul` of `OreLocalization` -/
@[irreducible]
protected def zsmul : ℤ → X[S⁻¹] → X[S⁻¹] := zsmulRec

Integer scalar multiplication on Ore localization

Informal description

The function defines integer scalar multiplication on the Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$. For any integer $n$ and any element $x \in X[S^{-1}]$, it returns $n \cdot x$ by repeated addition or subtraction.

OreLocalization.instAddGroupOreLocalization instance

: AddGroup X[S⁻¹]

Full source

instance instAddGroupOreLocalization : AddGroup X[S⁻¹] where
  neg_add_cancel := OreLocalization.neg_add_cancel
  zsmul := OreLocalization.zsmul

Additive Group Structure on Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$ forms an additive group.

OreLocalization.instAddCommGroup instance

: AddCommGroup X[S⁻¹]

Full source

instance : AddCommGroup X[S⁻¹] where
  __ := inferInstanceAs (AddGroup X[S⁻¹])
  __ := inferInstanceAs (AddCommMonoid X[S⁻¹])

Additive Commutative Group Structure on Ore Localization

Informal description

The Ore localization $X[S^{-1}]$ of a ring $X$ with respect to a left Ore set $S$ forms an additive commutative group.

Mathlib.RingTheory.OreLocalization.Basic

References

Tags