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} [OreLocalization.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} [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

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

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

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

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

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 ⋯ ⋯

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 ⋯ ⋯

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 ⋯ ⋯

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

@[simp]

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

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

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)) ⋯ ⋯

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 : { x : R // x ∈ S } →* Tˣ) (hf : ∀ (s : { x : R // x ∈ 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} [OreLocalization.OreSet S] {T : Type u_3} [Semiring T] (f : R →+* T) (fS : { x : R // x ∈ S } →* Tˣ) (hf : ∀ (s : { x : R // x ∈ S }), f ↑s = ↑(fS s)) {r : R} {s : { x : R // x ∈ S }} : (OreLocalization.universalHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r

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 : { x : R // x ∈ S } →* Tˣ) (hf : ∀ (s : { x : R // x ∈ S }), f ↑s = ↑(fS s)) {r : R} : (OreLocalization.universalHom f fS hf) (OreLocalization.numeratorHom r) = f r

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 : { x : R // x ∈ S } →* Tˣ) (hf : ∀ (s : { x : R // x ∈ S }), f ↑s = ↑(fS s)) (φ : OreLocalization S R →+* T) (huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) : φ = OreLocalization.universalHom f fS hf

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

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

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

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)

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

Equations

• ⋯ = ⋯

@[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 : { x : R // x ∈ nonZeroDivisors R }) => if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) ⋯

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 }

theorem OreLocalization.inv_def {R : Type u_1} [Ring R] [Nontrivial R] [OreLocalization.OreSet (nonZeroDivisors R)] [NoZeroDivisors R] {r : R} {s : { x : R // x ∈ nonZeroDivisors R }} : (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

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

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

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 (q : ℚ≥0) => HMul.hMul ↑q) ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯

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

Equations

• OreLocalization.instCommSemiring = CommSemiring.mk ⋯

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

Equations

• OreLocalization.instCommRing = CommRing.mk ⋯

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 ⋯