Module and Ring instances of Ore Localizations

The Monoid and DistribMulAction instances and additive versions are provided in Mathlib/RingTheory/OreLocalization/Basic.lean.

theorem OreLocalization.zero_smul {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddCommMonoid X] [Module R X] (x : OreLocalization S X) : 0 • x = 0

theorem OreLocalization.add_smul {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddCommMonoid X] [Module R X] (y z : OreLocalization S R) (x : OreLocalization S X) : (y + z) • x = y • x + z • x

@[deprecated MulZeroClass.zero_mul (since := "2025-08-20")]

theorem OreLocalization.zero_mul {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] (x : OreLocalization S R) : 0 * x = 0

@[deprecated MulZeroClass.mul_zero (since := "2025-08-20")]

theorem OreLocalization.mul_zero {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] (x : OreLocalization S R) : x * 0 = 0

theorem OreLocalization.left_distrib {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] (x y z : OreLocalization S R) : x * (y + z) = x * y + x * z

theorem OreLocalization.right_distrib {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] (x y z : OreLocalization S R) : (x + y) * z = x * z + y * z

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

Equations

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

instance OreLocalization.instModule {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddCommMonoid X] [Module R X] : Module (OreLocalization S R) (OreLocalization S X)

Equations

• OreLocalization.instModule = { toDistribMulAction := OreLocalization.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance OreLocalization.instModuleOfIsScalarTower {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddCommMonoid X] [Module R X] {R₀ : Type u_3} [Semiring R₀] [Module R₀ X] [Module R₀ R] [IsScalarTower R₀ R X] [IsScalarTower R₀ R R] : Module R₀ (OreLocalization S X)

Equations

• OreLocalization.instModuleOfIsScalarTower = { toDistribMulAction := OreLocalization.instDistribMulActionOfIsScalarTower, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem OreLocalization.nsmul_eq_nsmul {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddCommMonoid X] [Module R X] (n : ℕ) (x : OreLocalization S X) : n • x = n • x

def OreLocalization.numeratorRingHom {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] : R →+* OreLocalization S R

The ring homomorphism from R to R[S⁻¹], mapping r : R to the fraction r /ₒ 1.

Equations

• OreLocalization.numeratorRingHom = { toMonoidHom := OreLocalization.numeratorHom, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem OreLocalization.numeratorRingHom_apply {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] (r : R) : numeratorRingHom r = r /ₒ 1

instance OreLocalization.instAlgebra {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {R₀ : Type u_3} [CommSemiring R₀] [Algebra R₀ R] : Algebra R₀ (OreLocalization S R)

Equations

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

def OreLocalization.universalHom {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {T : Type u_3} [Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) : OreLocalization S R →+* T

The universal lift from a ring homomorphism f : R →+* T, which maps elements in S to units of T, to a ring homomorphism R[S⁻¹] →+* T. This extends the construction on monoids.

Equations

• OreLocalization.universalHom f fS hf = { toMonoidHom := OreLocalization.universalMulHom (↑f) fS hf, map_zero' := ⋯, map_add' := ⋯ }

theorem OreLocalization.universalHom_apply {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {T : Type u_3} [Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} {s : ↥S} : (universalHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r

theorem OreLocalization.universalHom_commutes {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {T : Type u_3} [Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} : (universalHom f fS hf) (numeratorHom r) = f r

theorem OreLocalization.universalHom_unique {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] {T : Type u_3} [Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : OreLocalization S R →+* T) (huniv : ∀ (r : R), φ (numeratorHom r) = f r) : φ = universalHom f fS hf

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

Equations

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

@[simp]

theorem OreLocalization.zsmul_eq_zsmul {R : Type u_1} [Ring R] {S : Submonoid R} [OreSet S] {X : Type u_2} [AddCommGroup X] [Module R X] (n : ℤ) (x : OreLocalization S X) : n • x = n • x

theorem OreLocalization.numeratorHom_inj {R : Type u_1} [Ring R] {S : Submonoid R} [OreSet S] (hS : S ≤ nonZeroDivisorsLeft R) : Function.Injective ⇑numeratorHom

instance OreLocalization.instDivisionRingNonZeroDivisors {R : Type u_1} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreSet (nonZeroDivisors R)] : DivisionRing (OreLocalization (nonZeroDivisors R) R)

Equations

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

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

Equations

• OreLocalization.instCommSemiring = { toSemiring := inferInstanceAs (Semiring (OreLocalization S R)), mul_comm := ⋯ }

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

Equations

• OreLocalization.instCommRing = { toRing := inferInstanceAs (Ring (OreLocalization S R)), mul_comm := ⋯ }

noncomputable instance OreLocalization.instFieldNonZeroDivisors {R : Type u_1} [CommRing R] [Nontrivial R] [NoZeroDivisors R] [OreSet (nonZeroDivisors R)] : Field (OreLocalization (nonZeroDivisors R) R)

Equations

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