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

source

@[reducible]

def is_localization.away {R : Type u_1} [comm_semiring R] (x : R) (S : Type u_2) [comm_semiring S] [algebra R 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.

source

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

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

Equations

is_localization.away.inv_self x = is_localization.mk' S 1 ⟨x, _⟩

source

@[simp]

theorem is_localization.away.mul_inv_self {R : Type u_1} [comm_semiring R] {S : Type u_2} [comm_semiring S] [algebra R S] (x : R) [is_localization.away x S] :

⇑(algebra_map R S) x * is_localization.away.inv_self x = 1

source

noncomputable def is_localization.away.lift {R : Type u_1} [comm_semiring R] {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] (x : R) [is_localization.away x 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

is_localization.away.lift x hg = is_localization.lift _

source

@[simp]

theorem is_localization.away.away_map.lift_eq {R : Type u_1} [comm_semiring R] {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (⇑g x)) (a : R) :

⇑(is_localization.away.lift x hg) (⇑(algebra_map R S) a) = ⇑g a

source

@[simp]

theorem is_localization.away.away_map.lift_comp {R : Type u_1} [comm_semiring R] {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] (x : R) [is_localization.away x S] {g : R →+* P} (hg : is_unit (⇑g x)) :

(is_localization.away.lift x hg).comp (algebra_map R S) = g

source

noncomputable def is_localization.away.away_to_away_right {R : Type u_1} [comm_semiring R] {S : Type u_2} [comm_semiring S] [algebra R S] {P : Type u_3} [comm_semiring P] (x : R) [is_localization.away x S] (y : R) [algebra 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

is_localization.away.away_to_away_right x y = is_localization.away.lift x _

source

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

is_localization.away.map S Q f r = is_localization.map Q f _

source

noncomputable def is_localization.at_units (R : Type u_1) [comm_semiring R] (M : submonoid R) (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization M S] (H : ∀ (x : ↥M), is_unit ↑x) :

R ≃ₐ[R] S

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

Equations

is_localization.at_units R M S H = alg_equiv.of_bijective (algebra.of_id R S) _

source

noncomputable def is_localization.at_unit (R : Type u_1) [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] (x : R) (e : is_unit x) [is_localization.away x S] :

R ≃ₐ[R] S

The localization away from a unit is isomorphic to the ring

Equations

is_localization.at_unit R S x e = is_localization.at_units R (submonoid.powers x) S _

source

noncomputable def is_localization.at_one (R : Type u_1) [comm_semiring R] (S : Type u_2) [comm_semiring S] [algebra R S] [is_localization.away 1 S] :

R ≃ₐ[R] S

The localization at one is isomorphic to the ring.

Equations

is_localization.at_one R S = is_localization.at_unit R S 1 _

source

theorem is_localization.away_of_is_unit_of_bijective {R : Type u_1} (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] {r : R} (hr : is_unit r) (H : function.bijective ⇑(algebra_map R S)) :

is_localization.away r S

source

@[reducible]

noncomputable def localization.away_lift {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (f : R →+* P) (r : R) (hr : is_unit (⇑f r)) :

localization.away r →+* P

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

source

@[reducible]

noncomputable def localization.away_map {R : Type u_1} [comm_semiring R] {P : Type u_3} [comm_semiring P] (f : R →+* P) (r : R) :

localization.away r →+* localization.away (⇑f r)

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

source

noncomputable def self_zpow {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] (m : ℤ) :

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

Equations

self_zpow x B m = dite (0 ≤ m) (λ (hm : 0 ≤ m), ⇑(algebra_map R B) x ^ m.nat_abs) (λ (hm : ¬0 ≤ m), is_localization.mk' B 1 (submonoid.pow x m.nat_abs))

source

theorem self_zpow_of_nonneg {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] {n : ℤ} (hn : 0 ≤ n) :

self_zpow x B n = ⇑(algebra_map R B) x ^ n.nat_abs

source

@[simp]

theorem self_zpow_coe_nat {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] (d : ℕ) :

self_zpow x B ↑d = ⇑(algebra_map R B) x ^ d

source

@[simp]

theorem self_zpow_zero {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] :

self_zpow x B 0 = 1

source

theorem self_zpow_of_neg {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] {n : ℤ} (hn : n < 0) :

self_zpow x B n = is_localization.mk' B 1 (submonoid.pow x n.nat_abs)

source

theorem self_zpow_of_nonpos {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] {n : ℤ} (hn : n ≤ 0) :

self_zpow x B n = is_localization.mk' B 1 (submonoid.pow x n.nat_abs)

source

@[simp]

theorem self_zpow_neg_coe_nat {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] (d : ℕ) :

self_zpow x B (-↑d) = is_localization.mk' B 1 (submonoid.pow x d)

source

@[simp]

theorem self_zpow_sub_cast_nat {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] {n m : ℕ} :

self_zpow x B (↑n - ↑m) = is_localization.mk' B (x ^ n) (submonoid.pow x m)

source

@[simp]

theorem self_zpow_add {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] {n m : ℤ} :

self_zpow x B (n + m) = self_zpow x B n * self_zpow x B m

source

theorem self_zpow_mul_neg {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] (d : ℤ) :

self_zpow x B d * self_zpow x B (-d) = 1

source

theorem self_zpow_neg_mul {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] (d : ℤ) :

self_zpow x B (-d) * self_zpow x B d = 1

source

theorem self_zpow_pow_sub {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] (a : R) (b : B) (m d : ℤ) :

self_zpow x B (m - d) * is_localization.mk' B a 1 = b ↔ self_zpow x B m * is_localization.mk' B a 1 = self_zpow x B d * b

source

theorem exists_reduced_fraction' {R : Type u_1} [comm_ring R] (x : R) (B : Type u_2) [comm_ring B] [algebra R B] [is_localization.away x B] [is_domain R] [normalization_monoid R] [unique_factorization_monoid R] {b : B} (hb : b ≠ 0) (hx : irreducible x) :

∃ (a : R) (n : ℤ), ¬x ∣ a ∧ self_zpow x B n * ⇑(algebra_map R B) a = b