Documentation

Mathlib.RingTheory.OreLocalization.Basic

Localization over left Ore sets. #

This file proves results on the localization of rings (monoids with zeros) over a left Ore set.

References #

Tags #

localization, Ore, non-commutative

source
@[simp]
theorem OreLocalization.zero_oreDiv' {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreLocalization.OreSet S] (s : ↥S) :
0 /ₒ s = 0
source
instance OreLocalization.instMonoidWithZero {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreLocalization.OreSet S] :
MonoidWithZero (OreLocalization S R)
Equations
source
instance OreLocalization.instCommMonoidWithZero {R : Type u_1} [CommMonoidWithZero R] {S : Submonoid R} [OreLocalization.OreSet S] :
CommMonoidWithZero (OreLocalization S R)
Equations
source
instance OreLocalization.instAdd {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] :
Add (OreLocalization S X)
Equations
  • OreLocalization.instAdd = { add := OreLocalization.add }
source
theorem OreLocalization.oreDiv_add_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} {s : ↥S} {s' : ↥S} :
r /ₒ s + r' /ₒ s' = (OreLocalization.oreDenom (↑s) s' • r + OreLocalization.oreNum (↑s) s' • r') /ₒ (OreLocalization.oreDenom (↑s) s' * s)
source
theorem OreLocalization.oreDiv_add_char' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} (s : ↥S) (s' : ↥S) (rb : R) (sb : R) (h : sb * ↑s = rb * ↑s') (h' : sb * ↑s ∈ S) :
r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩
source
theorem OreLocalization.oreDiv_add_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} (s : ↥S) (s' : ↥S) (rb : R) (sb : ↥S) (h : ↑sb * ↑s = rb * ↑s') :
r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s)

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

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

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

Equations
source
@[simp]
theorem OreLocalization.add_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} {s : ↥S} :
r /ₒ s + r' /ₒ s = (r + r') /ₒ s
source
theorem OreLocalization.add_assoc {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) (y : OreLocalization S X) (z : OreLocalization S X) :
x + y + z = x + (y + z)
source
@[simp]
theorem OreLocalization.zero_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (s : ↥S) :
0 /ₒ s = 0
source
theorem OreLocalization.zero_add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) :
0 + x = x
source
theorem OreLocalization.add_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) :
x + 0 = x
source
instance OreLocalization.instAddMonoid {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] :
AddMonoid (OreLocalization S X)
Equations
  • OreLocalization.instAddMonoid = AddMonoid.mk ⋯ ⋯ OreLocalization.nsmul ⋯ ⋯
source
theorem OreLocalization.smul_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S R) :
x • 0 = 0
source
theorem OreLocalization.smul_add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (z : OreLocalization S R) (x : OreLocalization S X) (y : OreLocalization S X) :
z • (x + y) = z • x + z • y
source
instance OreLocalization.instDistribMulAction {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] :
DistribMulAction (OreLocalization S R) (OreLocalization S X)
Equations
source
instance OreLocalization.instDistribMulActionOfIsScalarTower {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {R₀ : Type u_3} [Monoid R₀] [MulAction R₀ X] [MulAction R₀ R] [IsScalarTower R₀ R X] [IsScalarTower R₀ R R] :
DistribMulAction R₀ (OreLocalization S X)
Equations
source
theorem OreLocalization.add_comm {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommMonoid X] [DistribMulAction R X] (x : OreLocalization S X) (y : OreLocalization S X) :
x + y = y + x
source
instance OreLocalization.instAddCommMonoidOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommMonoid X] [DistribMulAction R X] :
AddCommMonoid (OreLocalization S X)
Equations
source
@[irreducible]
def OreLocalization.neg {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] :
OreLocalization S X → OreLocalization S X

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

Equations
source
instance OreLocalization.instNegOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] :
Neg (OreLocalization S X)
Equations
  • OreLocalization.instNegOreLocalization = { neg := OreLocalization.neg }
source
@[simp]
theorem OreLocalization.neg_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] (r : X) (s : ↥S) :
-(r /ₒ s) = -r /ₒ s
source
theorem OreLocalization.neg_add_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] (x : OreLocalization S X) :
-x + x = 0
source
@[irreducible]
def OreLocalization.zsmul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] :
ℤ → OreLocalization S X → OreLocalization S X

zsmul of OreLocalization

Equations
  • OreLocalization.zsmul = zsmulRec
source
instance OreLocalization.instAddGroupOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] :
AddGroup (OreLocalization S X)
Equations
  • OreLocalization.instAddGroupOreLocalization = AddGroup.mk ⋯
source
instance OreLocalization.instAddCommGroup {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommGroup X] [DistribMulAction R X] :
AddCommGroup (OreLocalization S X)
Equations