Localization over left Ore sets.

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

References

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

Tags

localization, Ore, non-commutative

@[simp]

theorem OreLocalization.zero_oreDiv' {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreLocalization.OreSet S] (s : ↥S) : 0 /ₒ s = 0

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

Equations

• OreLocalization.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

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

Equations

• OreLocalization.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

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

Equations

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

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

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

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

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

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

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

Equations

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

@[simp]

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

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

@[simp]

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

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

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

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

Equations

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

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

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

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

Equations

• OreLocalization.instDistribMulAction = DistribMulAction.mk ⋯ ⋯

instance OreLocalization.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

• OreLocalization.instDistribMulActionOfIsScalarTower = DistribMulAction.mk ⋯ ⋯

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

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

Equations

• OreLocalization.instAddCommMonoidOreLocalization = AddCommMonoid.mk ⋯

@[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

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

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

Equations

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

@[simp]

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

theorem OreLocalization.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

@[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

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

Equations

• OreLocalization.instAddGroupOreLocalization = AddGroup.mk ⋯

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

Equations

• OreLocalization.instAddCommGroup = AddCommGroup.mk ⋯