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}
[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}
[OreSet S]
{X : Type u_2}
[AddCommMonoid X]
[Module R X]
(y 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}
[OreSet S]
(x y z : OreLocalization S R)
:
x * (y + z) = x * y + x * z
theorem
OreLocalization.right_distrib
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreSet S]
(x y z : OreLocalization S R)
:
(x + y) * z = x * z + y * z
@[implicit_reducible]
instance
OreLocalization.instSemiring
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreSet S]
:
Semiring (OreLocalization S R)
@[implicit_reducible]
instance
OreLocalization.instModule
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreSet S]
{X : Type u_2}
[AddCommMonoid X]
[Module R X]
:
Module (OreLocalization S R) (OreLocalization S X)
@[implicit_reducible]
instance
OreLocalization.instModuleOfIsScalarTower
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[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}
[OreSet S]
{X : Type u_2}
[AddCommMonoid X]
[Module R X]
(n : โ)
(x : OreLocalization S X)
:
n โข x = n โข x
@[reducible, inline]
The ring homomorphism from R to R[Sโปยน], mapping r : R to the fraction r /โ 1.
Instances For
@[simp]
theorem
OreLocalization.numeratorRingHom_apply
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreSet S]
(r : R)
:
numeratorRingHom r = r /โ 1
@[implicit_reducible]
instance
OreLocalization.instAlgebra
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreSet S]
{Rโ : Type u_3}
[CommSemiring Rโ]
[Algebra Rโ R]
:
Algebra Rโ (OreLocalization S R)
def
OreLocalization.universalHom
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[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.
Instances For
theorem
OreLocalization.universalHom_commutes
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[OreSet S]
{T : Type u_3}
[Semiring T]
(f : R โ+* T)
(fS : โฅS โ* Tหฃ)
(hf : โ (s : โฅS), f โs = โ(fS s))
{r : R}
:
(universalHom f fS hf) (numeratorHom r) = f r
theorem
OreLocalization.universalHom_unique
{R : Type u_1}
[Semiring R]
{S : Submonoid R}
[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), ฯ (numeratorHom r) = f r)
:
ฯ = universalHom f fS hf
@[implicit_reducible]
instance
OreLocalization.instRing
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[OreSet S]
:
Ring (OreLocalization S R)
@[simp]
theorem
OreLocalization.zsmul_eq_zsmul
{R : Type u_1}
[Ring R]
{S : Submonoid R}
[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}
[OreSet S]
(hS : S โค nonZeroDivisorsLeft R)
:
Function.Injective โnumeratorHom
@[implicit_reducible]
noncomputable instance
OreLocalization.instDivisionRingNonZeroDivisors
{R : Type u_1}
[Ring R]
[Nontrivial R]
[NoZeroDivisors R]
[OreSet (nonZeroDivisors R)]
:
@[implicit_reducible]
instance
OreLocalization.instCommSemiring
{R : Type u_1}
[CommSemiring R]
{S : Submonoid R}
[OreSet S]
:
CommSemiring (OreLocalization S R)
@[implicit_reducible]
instance
OreLocalization.instCommRing
{R : Type u_1}
[CommRing R]
{S : Submonoid R}
[OreSet S]
:
CommRing (OreLocalization S R)
@[implicit_reducible]
noncomputable instance
OreLocalization.instFieldNonZeroDivisors
{R : Type u_1}
[CommRing R]
[Nontrivial R]
[NoZeroDivisors R]
[OreSet (nonZeroDivisors R)]
:
Field (OreLocalization (nonZeroDivisors R) R)