Localizations away from an element #
Main definitions #
IsLocalization.Away (x : R) S
expresses thatS
is a localization away fromx
, as an abbreviation ofIsLocalization (Submonoid.powers x) S
.exists_reduced_fraction' (hb : b ≠ 0)
produces a reduced fraction of the formb = a * x^n
for somen : ℤ
and somea : R
that is not divisible byx
.
Implementation notes #
See Mathlib/RingTheory/Localization/Basic.lean
for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
Given x : R
, the typeclass IsLocalization.Away x S
states that S
is
isomorphic to the localization of R
at the submonoid generated by x
.
See IsLocalization.Away.mk
for a specialized constructor.
Equations
- IsLocalization.Away x S = IsLocalization (Submonoid.powers x) S
Instances For
Given x : R
and a localization map F : R →+* S
away from x
, invSelf
is (F x)⁻¹
.
Equations
- IsLocalization.Away.invSelf x = IsLocalization.mk' S 1 ⟨x, ⋯⟩
Instances For
For s : S
with S
being the localization of R
away from x
,
this is a choice of (r, n) : R × ℕ
such that s * algebraMap R S (x ^ n) = algebraMap R S r
.
Equations
- IsLocalization.Away.sec x s = ((IsLocalization.sec (Submonoid.powers x) s).1, Exists.choose ⋯)
Instances For
Specialized constructor for IsLocalization.Away
.
If r
and r'
are associated elements of R
, an R
-algebra S
is the localization of R
away from r
if and only of it is the localization of R
away from
r'
.
Given x : R
, a localization map F : R →+* S
away from x
, and a map of CommSemiring
s
g : R →+* P
such that g x
is invertible, the homomorphism induced from S
to P
sending
z : S
to g y * (g x)⁻ⁿ
, where y : R, n : ℕ
are such that z = F y * (F x)⁻ⁿ
.
Equations
Instances For
Given x y : R
and localizations S
, P
away from x
and x * y
respectively, the homomorphism induced from S
to P
.
Equations
Instances For
Given a map f : R →+* S
and an element r : R
, we may construct a map Rᵣ →+* Sᵣ
.
Equations
- IsLocalization.Away.map S Q f r = IsLocalization.map Q f ⋯
Instances For
Equations
- ⋯ = ⋯
Given a algebra map f : A →ₐ[R] B
and an element a : A
, we may construct a map
Aₐ →ₐ[R] Bₐ
.
Equations
- IsLocalization.Away.mapₐ Aₚ Bₚ f a = { toRingHom := IsLocalization.Away.map Aₚ Bₚ f.toRingHom a, commutes' := ⋯ }
Instances For
Localizing the localization of R
at x
at the image of y
is the same as localizing
R
at y * x
. See IsLocalization.Away.mul'
for the x * y
version.
Localizing the localization of R
at x
at the image of y
is the same as localizing
R
at x * y
. See IsLocalization.Away.mul
for the y * x
version.
If S₁
is the localization of R
away from f
and S₂
is the localization away from g
,
then any localization T
of S₂
away from f
is also a localization of S₁
away from g
.
The localization away from a unit is isomorphic to the ring.
Equations
- IsLocalization.atUnit R S x e = IsLocalization.atUnits R (Submonoid.powers x) ⋯
Instances For
The localization at one is isomorphic to the ring.
Equations
- IsLocalization.atOne R S = IsLocalization.atUnit R S 1 ⋯
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Given a map f : R →+* S
and an element r : R
, such that f r
is invertible,
we may construct a map Rᵣ →+* S
.
Equations
- Localization.awayLift f r hr = IsLocalization.Away.lift r hr
Instances For
Given a map f : R →+* S
and an element r : R
, we may construct a map Rᵣ →+* Sᵣ
.
Equations
- Localization.awayMap f r = IsLocalization.Away.map (Localization.Away r) (Localization.Away (f r)) f r
Instances For
Given a map f : A →ₐ[R] B
and an element a : A
, we may construct a map Aₐ →ₐ[R] Bₐ
.
Equations
- Localization.awayMapₐ f a = IsLocalization.Away.mapₐ (Localization.Away a) (Localization.Away (f a)) f a
Instances For
selfZPow x (m : ℤ)
is x ^ m
as an element of the localization away from x
.
Equations
- selfZPow x B m = if x_1 : 0 ≤ m then (algebraMap R B) x ^ m.natAbs else IsLocalization.mk' B 1 (Submonoid.pow x m.natAbs)
Instances For
Alias of selfZPow_natCast
.
Alias of selfZPow_neg_natCast
.
Alias of selfZPow_sub_natCast
.