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)
:
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)
:
theorem
OreLocalization.zero_mul
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization S R)
:
theorem
OreLocalization.mul_zero
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(x : OreLocalization S R)
:
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)
:
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)
:
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)
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)
@[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)
:
@[simp]
theorem
OreLocalization.numeratorRingHom_apply
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
(r : R)
:
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
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 : ↥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
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)
:
φ = OreLocalization.universalHom f fS hf
instance
OreLocalization.instRing
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreLocalization.OreSet S]
:
Ring (OreLocalization S R)
@[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)
:
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 : ↥(nonZeroDivisors R)) => if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) ⋯
Instances For
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 : ↥(nonZeroDivisors 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)
:
theorem
OreLocalization.inv_zero
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
:
instance
OreLocalization.instDivisionRingNonZeroDivisors
{R : Type u_1}
[Ring R]
[Nontrivial R]
[OreLocalization.OreSet (nonZeroDivisors R)]
[NoZeroDivisors R]
:
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)