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} [OreLocalization.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} [OreLocalization.OreSet S] {X : Type u_2} [AddCommMonoid X] [Module R X] (y : OreLocalization S R) (z : OreLocalization S R) (x : OreLocalization S X) :

(y + z) • x = y • x + z • x

source

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

0 * x = 0

source

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

x * 0 = 0

source

theorem OreLocalization.left_distrib {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization S R) (y : OreLocalization S R) (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} [OreLocalization.OreSet S] (x : OreLocalization S R) (y : OreLocalization S R) (z : OreLocalization S R) :

(x + y) * z = x * z + y * z

source

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

Semiring (OreLocalization S R)

Equations

OreLocalization.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

source

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

Module (OreLocalization S R) (OreLocalization S X)

Equations

OreLocalization.instModule = Module.mk ⋯ ⋯

source

instance OreLocalization.instModuleOfIsScalarTower {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.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 = Module.mk ⋯ ⋯

source

@[simp]

theorem OreLocalization.nsmul_eq_nsmul {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.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} [OreLocalization.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} [OreLocalization.OreSet S] (r : R) :

OreLocalization.numeratorRingHom r = r /ₒ 1

source

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

Algebra R₀ (OreLocalization S R)

Equations

OreLocalization.instAlgebra = Algebra.mk (OreLocalization.numeratorRingHom.comp (algebraMap R₀ R)) ⋯ ⋯

source

def OreLocalization.universalHom {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.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} [OreLocalization.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} :

(OreLocalization.universalHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r

source

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

(OreLocalization.universalHom f fS hf) (OreLocalization.numeratorHom r) = f r

source

theorem OreLocalization.universalHom_unique {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.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), φ (OreLocalization.numeratorHom r) = f r) :

φ = OreLocalization.universalHom f fS hf

source

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

Ring (OreLocalization S R)

Equations

OreLocalization.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

@[simp]

theorem OreLocalization.zsmul_eq_zsmul {R : Type u_1} [Ring R] {S : Submonoid R} [OreLocalization.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} [OreLocalization.OreSet S] (hS : S ≤ nonZeroDivisorsRight R) :

Function.Injective ⇑OreLocalization.numeratorHom

source

theorem OreLocalization.subsingleton_iff {R : Type u_1} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] :

Subsingleton (OreLocalization S R) ↔ 0 ∈ S

source

theorem OreLocalization.nontrivial_iff {R : Type u_1} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] :

Nontrivial (OreLocalization S R) ↔ 0 ∉ S

source

theorem OreLocalization.nontrivial_of_nonZeroDivisors {R : Type u_1} [Ring R] {S : Submonoid R} [OreLocalization.OreSet S] [Nontrivial R] (hS : S ≤ nonZeroDivisors R) :

Nontrivial (OreLocalization S R)

source

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

Nontrivial (OreLocalization (nonZeroDivisors R) R)

Equations

⋯ = ⋯

source

@[irreducible]

def OreLocalization.inv {R : Type u_1} [Ring R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :

OreLocalization (nonZeroDivisors R) R → OreLocalization (nonZeroDivisors R) R

The inversion of Ore fractions for a ring without zero divisors, satisfying 0⁻¹ = 0 and (r /ₒ r')⁻¹ = r' /ₒ r for r ≠ 0.

Equations

OreLocalization.inv = OreLocalization.liftExpand (fun (r : R) (s : ↥(nonZeroDivisors R)) => if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) ⋯

Instances For

source

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

Inv (OreLocalization (nonZeroDivisors R) R)

Equations

OreLocalization.inv' = { inv := OreLocalization.inv }

source

theorem OreLocalization.inv_def {R : Type u_1} [Ring R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] {r : R} {s : ↥(nonZeroDivisors R)} :

(r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

source

theorem OreLocalization.mul_inv_cancel {R : Type u_1} [Ring R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] (x : OreLocalization (nonZeroDivisors R) R) (h : x ≠ 0) :

x * x⁻¹ = 1

source

theorem OreLocalization.inv_zero {R : Type u_1} [Ring R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] :

0⁻¹ = 0

source

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

DivisionRing (OreLocalization (nonZeroDivisors R) R)

Equations

OreLocalization.instDivisionRingNonZeroDivisors = DivisionRing.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

source

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

CommSemiring (OreLocalization S R)

Equations

OreLocalization.instCommSemiring = CommSemiring.mk ⋯

source

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

CommRing (OreLocalization S R)

Equations

OreLocalization.instCommRing = CommRing.mk ⋯

source

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

Field (OreLocalization (nonZeroDivisors R) R)

Equations

OreLocalization.instFieldNonZeroDivisors = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯

Documentation

Mathlib.RingTheory.OreLocalization.Ring

Module and Ring instances of Ore Localizations #