# Localizations away from an element #

## Main definitions #

• IsLocalization.Away (x : R) S expresses that S is a localization away from x, as an abbreviation of IsLocalization (Submonoid.powers x) S.
• exists_reduced_fraction' (hb : b ≠ 0) produces a reduced fraction of the form b = a * x^n for some n : ℤ and some a : R that is not divisible by x.

## 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

@[reducible, inline]
abbrev IsLocalization.Away {R : Type u_1} [] (x : R) (S : Type u_4) [] [Algebra R S] :

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.

Equations
Instances For
noncomputable def IsLocalization.Away.invSelf {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (x : R) [] :
S

Given x : R and a localization map F : R →+* S away from x, invSelf is (F x)⁻¹.

Equations
Instances For
@[simp]
theorem IsLocalization.Away.mul_invSelf {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] (x : R) [] :
() x * = 1
noncomputable def IsLocalization.Away.lift {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] (x : R) [] {g : R →+* P} (hg : IsUnit (g x)) :
S →+* P

Given x : R, a localization map F : R →+* S away from x, and a map of CommSemirings 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
@[simp]
theorem IsLocalization.Away.AwayMap.lift_eq {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] (x : R) [] {g : R →+* P} (hg : IsUnit (g x)) (a : R) :
() (() a) = g a
@[simp]
theorem IsLocalization.Away.AwayMap.lift_comp {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] (x : R) [] {g : R →+* P} (hg : IsUnit (g x)) :
().comp () = g
noncomputable def IsLocalization.Away.awayToAwayRight {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {P : Type u_3} [] (x : R) [] (y : R) [Algebra R P] [IsLocalization.Away (x * y) P] :
S →+* P

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
noncomputable def IsLocalization.Away.map {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {P : Type u_3} [] (Q : Type u_4) [] [Algebra P Q] (f : R →+* P) (r : R) [] [IsLocalization.Away (f r) Q] :
S →+* Q

Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.

Equations
Instances For
noncomputable def IsLocalization.atUnit (R : Type u_1) [] (S : Type u_2) [] [Algebra R S] (x : R) (e : ) [] :

The localization away from a unit is isomorphic to the ring.

Equations
Instances For
noncomputable def IsLocalization.atOne (R : Type u_1) [] (S : Type u_2) [] [Algebra R S] [] :

The localization at one is isomorphic to the ring.

Equations
Instances For
theorem IsLocalization.away_of_isUnit_of_bijective {R : Type u_4} (S : Type u_5) [] [] [Algebra R S] {r : R} (hr : ) (H : Function.Bijective ()) :
@[reducible, inline]
noncomputable abbrev Localization.awayLift {R : Type u_1} [] {P : Type u_3} [] (f : R →+* P) (r : R) (hr : IsUnit (f r)) :

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
Instances For
@[reducible, inline]
noncomputable abbrev Localization.awayMap {R : Type u_1} [] {P : Type u_3} [] (f : R →+* P) (r : R) :

Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.

Equations
Instances For
noncomputable def selfZPow {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (m : ) :
B

selfZPow x (m : ℤ) is x ^ m as an element of the localization away from x.

Equations
Instances For
theorem selfZPow_of_nonneg {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] {n : } (hn : 0 n) :
selfZPow x B n = () x ^ n.natAbs
@[simp]
theorem selfZPow_natCast {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (d : ) :
selfZPow x B d = () x ^ d
@[simp]
theorem selfZPow_zero {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] :
selfZPow x B 0 = 1
theorem selfZPow_of_neg {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] {n : } (hn : n < 0) :
theorem selfZPow_of_nonpos {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] {n : } (hn : n 0) :
@[simp]
theorem selfZPow_neg_natCast {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (d : ) :
selfZPow x B (-d) = IsLocalization.mk' B 1 ()
@[simp]
theorem selfZPow_sub_natCast {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] {n : } {m : } :
selfZPow x B (n - m) = IsLocalization.mk' B (x ^ n) ()
@[deprecated selfZPow_natCast]
theorem selfZPow_coe_nat {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (d : ) :
selfZPow x B d = () x ^ d

Alias of selfZPow_natCast.

@[deprecated selfZPow_neg_natCast]
theorem selfZPow_neg_coe_nat {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (d : ) :
selfZPow x B (-d) = IsLocalization.mk' B 1 ()

Alias of selfZPow_neg_natCast.

@[deprecated selfZPow_sub_natCast]
theorem selfZPow_sub_cast_nat {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] {n : } {m : } :
selfZPow x B (n - m) = IsLocalization.mk' B (x ^ n) ()

Alias of selfZPow_sub_natCast.

@[simp]
theorem selfZPow_add {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] {n : } {m : } :
selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
theorem selfZPow_mul_neg {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (d : ) :
selfZPow x B d * selfZPow x B (-d) = 1
theorem selfZPow_neg_mul {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (d : ) :
selfZPow x B (-d) * selfZPow x B d = 1
theorem selfZPow_pow_sub {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] (a : R) (b : B) (m : ) (d : ) :
selfZPow x B (m - d) * = b selfZPow x B m * = selfZPow x B d * b
theorem exists_reduced_fraction' {R : Type u_1} [] (x : R) (B : Type u_2) [] [Algebra R B] [] [] [] {b : B} (hb : b 0) (hx : ) :
∃ (a : R) (n : ), ¬x a selfZPow x B n * () a = b