Documentation

Mathlib.RingTheory.OreLocalization.Ring

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.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
Equations
  • OreLocalization.instSemiring = Semiring.mk Monoid.npow
Equations
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] :
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

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
    instance OreLocalization.instAlgebra {R : Type u_1} [Semiring R] {S : Submonoid R} [OreLocalization.OreSet S] {R₀ : Type u_3} [CommSemiring R₀] [Algebra R₀ 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 : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) :

    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
    Instances For
      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
      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
      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) :
      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
      @[irreducible]

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

      Equations
      Instances For
        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 : (nonZeroDivisors R)} :
        (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else s /ₒ r,
        Equations
        Equations
        Equations
        Equations
        • OreLocalization.instFieldNonZeroDivisors = Field.mk DivisionRing.zpow DivisionRing.nnqsmul DivisionRing.qsmul