# mathlib3documentation

ring_theory.localization.away.basic

# Localizations away from an element #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• is_localization.away (x : R) S expresses that S is a localization away from x, as an abbreviation of is_localization (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 src/ring_theory/localization/basic.lean for a design overview.

## Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

@[reducible]
def is_localization.away {R : Type u_1} (x : R) (S : Type u_2) [ S] :
Prop

Given x : R, the typeclass is_localization.away x S states that S is isomorphic to the localization of R at the submonoid generated by x.

noncomputable def is_localization.away.inv_self {R : Type u_1} {S : Type u_2} [ S] (x : R) [ S] :
S

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

Equations
@[simp]
theorem is_localization.away.mul_inv_self {R : Type u_1} {S : Type u_2} [ S] (x : R) [ S] :
= 1
noncomputable def is_localization.away.lift {R : Type u_1} {S : Type u_2} [ S] {P : Type u_3} (x : R) [ S] {g : R →+* P} (hg : is_unit (g x)) :
S →+* P

Given x : R, a localization map F : R →+* S away from x, and a map of comm_semirings 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
@[simp]
theorem is_localization.away.away_map.lift_eq {R : Type u_1} {S : Type u_2} [ S] {P : Type u_3} (x : R) [ S] {g : R →+* P} (hg : is_unit (g x)) (a : R) :
( S) a) = g a
@[simp]
theorem is_localization.away.away_map.lift_comp {R : Type u_1} {S : Type u_2} [ S] {P : Type u_3} (x : R) [ S] {g : R →+* P} (hg : is_unit (g x)) :
.comp S) = g
noncomputable def is_localization.away.away_to_away_right {R : Type u_1} {S : Type u_2} [ S] {P : Type u_3} (x : R) [ S] (y : R) [ P] [is_localization.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
noncomputable def is_localization.away.map {R : Type u_1} (S : Type u_2) [ S] {P : Type u_3} (Q : Type u_4) [ Q] (f : R →+* P) (r : R) [ S] [ Q] :
S →+* Q

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

Equations
• r = _
noncomputable def is_localization.at_units (R : Type u_1) (M : submonoid R) (S : Type u_2) [ S] [ S] (H : (x : M), ) :

The localization at a module of units is isomorphic to the ring

Equations
• H =
noncomputable def is_localization.at_unit (R : Type u_1) (S : Type u_2) [ S] (x : R) (e : is_unit x) [ S] :

The localization away from a unit is isomorphic to the ring

Equations
• e = _
noncomputable def is_localization.at_one (R : Type u_1) (S : Type u_2) [ S] [ S] :

The localization at one is isomorphic to the ring.

Equations
• = _
theorem is_localization.away_of_is_unit_of_bijective {R : Type u_1} (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {r : R} (hr : is_unit r) (H : function.bijective S)) :
@[reducible]
noncomputable def localization.away_lift {R : Type u_1} {P : Type u_3} (f : R →+* P) (r : R) (hr : is_unit (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.

@[reducible]
noncomputable def localization.away_map {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ᵣ.

noncomputable def self_zpow {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] (m : ) :
B

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

Equations
theorem self_zpow_of_nonneg {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] {n : } (hn : 0 n) :
B n = B) x ^ n.nat_abs
@[simp]
theorem self_zpow_coe_nat {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] (d : ) :
B d = B) x ^ d
@[simp]
theorem self_zpow_zero {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] :
B 0 = 1
theorem self_zpow_of_neg {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] {n : } (hn : n < 0) :
B n = n.nat_abs)
theorem self_zpow_of_nonpos {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] {n : } (hn : n 0) :
B n = n.nat_abs)
@[simp]
theorem self_zpow_neg_coe_nat {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] (d : ) :
B (-d) = d)
@[simp]
theorem self_zpow_sub_cast_nat {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] {n m : } :
B (n - m) = (x ^ n) m)
@[simp]
theorem self_zpow_add {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] {n m : } :
B (n + m) = B n * B m
theorem self_zpow_mul_neg {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] (d : ) :
B d * B (-d) = 1
theorem self_zpow_neg_mul {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] (d : ) :
B (-d) * B d = 1
theorem self_zpow_pow_sub {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] (a : R) (b : B) (m d : ) :
B (m - d) * 1 = b B m * 1 = B d * b
theorem exists_reduced_fraction' {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [ B] [ B] [is_domain R] {b : B} (hb : b 0) (hx : irreducible x) :
(a : R) (n : ), ¬x a B n * B) a = b