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

source

@[reducible, inline]

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

Instances For

source

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] :

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

source

@[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

source

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

R × ℕ

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

source

theorem IsLocalization.Away.sec_spec {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] (s : S) :

s * (algebraMap R S) (x ^ (IsLocalization.Away.sec x s).2) = (algebraMap R S) (IsLocalization.Away.sec x s).1

source

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 ⋯

Instances For

source

@[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

source

@[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)) :

(IsLocalization.Away.lift x hg).comp (algebraMap R S) = g

source

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 ⋯

Instances For

source

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 ⋯

Instances For

source

instance IsLocalization.Away.instMapRingHomPowersOfCoe {A : Type u_5} [CommRing A] {B : Type u_6} [CommRing B] (Bₚ : Type u_8) [CommRing Bₚ] [Algebra B Bₚ] {f : A →+* B} (a : A) [IsLocalization.Away (f a) Bₚ] :

IsLocalization (Submonoid.map f (Submonoid.powers a)) Bₚ

Equations

⋯ = ⋯

source

noncomputable def IsLocalization.Away.mapₐ {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommRing A] [Algebra R A] {B : Type u_6} [CommRing B] [Algebra R B] (Aₚ : Type u_7) [CommRing Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommRing Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] :

Aₚ →ₐ[R] Bₚ

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

source

@[simp]

theorem IsLocalization.Away.mapₐ_apply {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommRing A] [Algebra R A] {B : Type u_6} [CommRing B] [Algebra R B] (Aₚ : Type u_7) [CommRing Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommRing Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (x : Aₚ) :

(IsLocalization.Away.mapₐ Aₚ Bₚ f a) x = (IsLocalization.Away.map Aₚ Bₚ f.toRingHom a) x

source

theorem IsLocalization.Away.mapₐ_injective_of_injective {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommRing A] [Algebra R A] {B : Type u_6} [CommRing B] [Algebra R B] {Aₚ : Type u_7} [CommRing Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] {Bₚ : Type u_8} [CommRing Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (hf : Function.Injective ⇑f) :

Function.Injective ⇑(IsLocalization.Away.mapₐ Aₚ Bₚ f a)

source

theorem IsLocalization.Away.mapₐ_surjective_of_surjective {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommRing A] [Algebra R A] {B : Type u_6} [CommRing B] [Algebra R B] {Aₚ : Type u_7} [CommRing Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] {Bₚ : Type u_8} [CommRing Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (hf : Function.Surjective ⇑f) :

Function.Surjective ⇑(IsLocalization.Away.mapₐ Aₚ Bₚ f a)

source

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) ⋯

Instances For

source

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 ⋯

Instances For

source

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

source

theorem IsLocalization.away_of_isIdempotentElem {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] {e : R} (he : IsIdempotentElem e) (H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}) (H' : Function.Surjective ⇑(algebraMap R S)) :

IsLocalization.Away e S

source

instance IsLocalization.away_fst {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] :

IsLocalization.Away (1, 0) R

Equations

⋯ = ⋯

source

instance IsLocalization.away_snd {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] :

IsLocalization.Away (0, 1) S

Equations

⋯ = ⋯

source

@[reducible, inline]

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

Instances For

source

@[reducible, inline]

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

Instances For

source

@[reducible, inline]

noncomputable abbrev Localization.awayMapₐ {R : Type u_1} [CommSemiring R] {A : Type u_4} [CommRing A] [Algebra R A] {B : Type u_5} [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (a : A) :

Localization.Away a →ₐ[R] Localization.Away (f a)

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

source

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 : ℤ) :

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

source

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 ^ n.natAbs

source

@[simp]

theorem selfZPow_natCast {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

source

@[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

source

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 n.natAbs)

source

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 n.natAbs)

source

@[simp]

theorem selfZPow_neg_natCast {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)

source

@[simp]

theorem selfZPow_sub_natCast {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)

source

@[deprecated selfZPow_natCast]

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

Alias of selfZPow_natCast.

source

@[deprecated selfZPow_neg_natCast]

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)

Alias of selfZPow_neg_natCast.

source

@[deprecated selfZPow_sub_natCast]

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)

Alias of selfZPow_sub_natCast.

source

@[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

source

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

source

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

source

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

source

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] [WfDvdMonoid R] {b : B} (hb : b ≠ 0) (hx : Irreducible x) :

∃ (a : R) (n : ℤ), ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b

Documentation

Mathlib.RingTheory.Localization.Away.Basic

Localizations away from an element #

Main definitions #

Implementation notes #

Tags #