# Module and Ring instances of Ore Localizations #

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

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

source
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 := ⋯ }

source
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 := ⋯ }

source
@[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
source
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' := ⋯ }

Instances For

source
@[simp]
theorem OreLocalization.numeratorRingHom_apply {R : Type u_1} [Semiring R] {S : Submonoid R} [OreSet S] (r : R) :
numeratorRingHom r = r /ₒ 1
source
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.

source
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' := ⋯ }

Instances For

source
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
source
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
source
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
source
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.

source
@[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
source
theorem OreLocalization.numeratorHom_inj {R : Type u_1} [Ring R] {S : Submonoid R} [OreSet S] (hS : S ≤ nonZeroDivisorsLeft R) :
Function.Injective ⇑numeratorHom
source
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.

source
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 := ⋯ }

source
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 := ⋯ }

source
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.