mathlib documentation

ring_theory.localization.away

Localizations away from an element #

Main definitions #

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

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.

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

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

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

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

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

The localization away from a unit is isomorphic to the ring

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

The localization at one is isomorphic to the ring.

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

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

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

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