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 = let __spread.0 := inferInstanceAs (Monoid (OreLocalization S R)); 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)
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 = let __src := OreLocalization.universalMulHom (↑f) fS hf; { toMonoidHom := __src, 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)
Equations
- One or more equations did not get rendered due to their size.
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
- ⋯ = ⋯
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, satisying 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]
: