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} [OreSet S] (s : ↥S) : 0 /ₒ s = 0

@[implicit_reducible]

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

Equations

• OreLocalization.instMonoidWithZero = { toMonoid := OreLocalization.instMonoid, toZero := OreLocalization.instZero, zero_mul := ⋯, mul_zero := ⋯ }

theorem OreLocalization.subsingleton_iff {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreSet S] : Subsingleton (OreLocalization S R) ↔ 0 ∈ S

theorem OreLocalization.nontrivial_iff {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreSet S] : Nontrivial (OreLocalization S R) ↔ ¬0 ∈ S

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

def OreLocalization.add'' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S) : OreLocalization S X

Auxiliary definition for addition on the Ore localization.

Equations

• OreLocalization.add'' r₁ s₁ r₂ s₂ = (OreLocalization.oreDenom (↑s₁) s₂ • r₁ + OreLocalization.oreNum (↑s₁) s₂ • r₂) /ₒ (OreLocalization.oreDenom (↑s₁) s₂ * s₁)

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

def OreLocalization.add' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (r₂ : X) (s₂ : ↥S) : OreLocalization S X → OreLocalization S X

Auxiliary definition for addition on the Ore localization, with one argument fixed.

Equations

• OreLocalization.add' r₂ s₂ = Quotient.lift (fun (r₁s₁ : X × ↥S) => OreLocalization.add'' r₁s₁.fst r₁s₁.snd r₂ s₂) ⋯

@[irreducible]

def OreLocalization.add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : OreLocalization S X → OreLocalization S X → OreLocalization S X

The addition on the Ore localization.

Equations

• x.add = Quotient.lift (fun (rs : X × ↥S) => OreLocalization.add' rs.fst rs.snd x) ⋯

@[implicit_reducible]

instance OreLocalization.instAdd {R : Type u_1} [Monoid R] {S : Submonoid R} [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} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r r' : X} {s s' : ↥S} : r /ₒ s + r' /ₒ s' = (oreDenom (↑s) s' • r + oreNum (↑s) s' • r') /ₒ (oreDenom (↑s) s' * s)

theorem OreLocalization.oreDiv_add_char' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r r' : X} (s s' : ↥S) (rb 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} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {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)

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

def OreLocalization.oreDivAddChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (r r' : X) (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} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r r' : X} {s : ↥S} : r /ₒ s + r' /ₒ s = (r + r') /ₒ s

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

@[simp]

theorem OreLocalization.zero_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [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} [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} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) : x + 0 = x

@[irreducible]

def OreLocalization.nsmul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] : ℕ → OreLocalization S X → OreLocalization S X

Scalar multiplication by natural numbers on the Ore localization.

Equations

• OreLocalization.nsmul = nsmulRec

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

theorem OreLocalization.smul_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [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} [OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (z : OreLocalization S R) (x y : OreLocalization S X) : z • (x + y) = z • x + z • y

@[implicit_reducible]

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

Equations

• OreLocalization.instDistribMulAction = { toMulAction := OreLocalization.instMulActionOreLocalization, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance OreLocalization.instDistribMulActionOfIsScalarTower {R : Type u_1} [Monoid R] {S : Submonoid R} [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 = { toMulAction := OreLocalization.instMulActionOfIsScalarTower, smul_zero := ⋯, smul_add := ⋯ }

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

@[implicit_reducible]

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

Equations

• OreLocalization.instAddCommMonoidOreLocalization = { toAddMonoid := OreLocalization.instAddMonoid, add_comm := ⋯ }

@[irreducible]

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

@[implicit_reducible]

instance OreLocalization.instNegOreLocalization {R : Type u_1} [Monoid R] {S : Submonoid R} [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} [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} [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} [OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] : ℤ → OreLocalization S X → OreLocalization S X

zsmul of OreLocalization

Equations

• OreLocalization.zsmul = zsmulRec

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OreLocalization.instAddCommGroup = { toAddGroup := inferInstanceAs (AddGroup (OreLocalization S X)), add_comm := ⋯ }