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

@[inline, reducible]

abbrev IsLocalization.Away {R : Type u_1} [CommSemiring R] (x : R) (S : Type u_4) [CommSemiring S] [Algebra R S] : Prop

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

• IsLocalization.Away x S = IsLocalization (Submonoid.powers x) S

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

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 { val := x, property := (_ : x ∈ Submonoid.powers x) }

@[simp]

theorem IsLocalization.Away.mul_invSelf {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] : ↑(algebraMap R S) x * IsLocalization.Away.invSelf x = 1

noncomputable def IsLocalization.Away.lift {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {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

• IsLocalization.Away.lift x hg = IsLocalization.lift (_ : ∀ (y : { x // x ∈ Submonoid.powers x }), IsUnit (↑g ↑y))

@[simp]

theorem IsLocalization.Away.AwayMap.lift_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (↑g x)) (a : R) : ↑(IsLocalization.Away.lift x hg) (↑(algebraMap R S) a) = ↑g a

@[simp]

theorem IsLocalization.Away.AwayMap.lift_comp {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (↑g x)) : RingHom.comp (IsLocalization.Away.lift x hg) (algebraMap R S) = g

noncomputable def IsLocalization.Away.awayToAwayRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] (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

• IsLocalization.Away.awayToAwayRight x y = IsLocalization.Away.lift x (_ : IsUnit (↑(algebraMap R P) x))

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

• IsLocalization.Away.map S Q f r = IsLocalization.map Q f (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r)))

noncomputable def IsLocalization.atUnits (R : Type u_1) [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (H : ∀ (x : { x // x ∈ M }), IsUnit ↑x) : R ≃ₐ[R] S

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

Equations

• IsLocalization.atUnits R M S H = AlgEquiv.ofBijective (Algebra.ofId R S) (_ : Function.Injective ↑(Algebra.ofId R S) ∧ Function.Surjective ↑(Algebra.ofId R S))

noncomputable def IsLocalization.atUnit (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (x : R) (e : IsUnit x) [IsLocalization.Away x S] : R ≃ₐ[R] S

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

Equations

• IsLocalization.atUnit R S x e = IsLocalization.atUnits R (Submonoid.powers x) S (_ : ∀ (x : { x // x ∈ Submonoid.powers x }), IsUnit ↑x)

noncomputable def IsLocalization.atOne (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization.Away 1 S] : R ≃ₐ[R] S

The localization at one is isomorphic to the ring.

Equations

• IsLocalization.atOne R S = IsLocalization.atUnit R S 1 (_ : IsUnit 1)

theorem IsLocalization.away_of_isUnit_of_bijective {R : Type u_4} (S : Type u_5) [CommRing R] [CommRing S] [Algebra R S] {r : R} (hr : IsUnit r) (H : Function.Bijective ↑(algebraMap R S)) : IsLocalization.Away r S

@[inline, reducible]

noncomputable abbrev Localization.awayLift {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : R →+* P) (r : R) (hr : IsUnit (↑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.

Equations

• Localization.awayLift f r hr = IsLocalization.Away.lift r hr

@[inline, reducible]

noncomputable abbrev Localization.awayMap {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring 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ᵣ.

Equations

• Localization.awayMap f r = IsLocalization.Away.map (Localization.Away r) (Localization.Away (↑f r)) f r

noncomputable def selfZpow {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (m : ℤ) : B

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

Equations

• selfZpow x B m = if x : 0 ≤ m then ↑(algebraMap R B) x ^ Int.natAbs m else IsLocalization.mk' B 1 (Submonoid.pow x (Int.natAbs m))

theorem selfZpow_of_nonneg {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} (hn : 0 ≤ n) : selfZpow x B n = ↑(algebraMap R B) x ^ Int.natAbs n

@[simp]

theorem selfZpow_coe_nat {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (d : ℕ) : selfZpow x B ↑d = ↑(algebraMap R B) x ^ d

@[simp]

theorem selfZpow_zero {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] : selfZpow x B 0 = 1

theorem selfZpow_of_neg {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} (hn : n < 0) : selfZpow x B n = IsLocalization.mk' B 1 (Submonoid.pow x (Int.natAbs n))

theorem selfZpow_of_nonpos {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} (hn : n ≤ 0) : selfZpow x B n = IsLocalization.mk' B 1 (Submonoid.pow x (Int.natAbs n))

@[simp]

theorem selfZpow_neg_coe_nat {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (d : ℕ) : selfZpow x B (-↑d) = IsLocalization.mk' B 1 (Submonoid.pow x d)

@[simp]

theorem selfZpow_sub_cast_nat {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : ℕ} {m : ℕ} : selfZpow x B (↑n - ↑m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)

@[simp]

theorem selfZpow_add {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} {m : ℤ} : selfZpow x B (n + m) = selfZpow x B n * selfZpow x B m

theorem selfZpow_mul_neg {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (d : ℤ) : selfZpow x B d * selfZpow x B (-d) = 1

theorem selfZpow_neg_mul {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (d : ℤ) : selfZpow x B (-d) * selfZpow x B d = 1

theorem selfZpow_pow_sub {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (a : R) (b : B) (m : ℤ) (d : ℤ) : selfZpow x B (m - d) * IsLocalization.mk' B a 1 = b ↔ selfZpow x B m * IsLocalization.mk' B a 1 = selfZpow x B d * b

theorem exists_reduced_fraction' {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {b : B} (hb : b ≠ 0) (hx : Irreducible x) : ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b