# mathlibdocumentation

ring_theory.localization.as_subring

# Localizations of domains as subalgebras of the fraction field. #

Given a domain A with fraction field K, and a submonoid S of A which does not contain zero, this file constructs the localization of A at S as a subalgebra of the field K over A.

theorem localization.map_is_unit_of_le {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] (hS : S ) (s : S) :
noncomputable def localization.map_to_fraction_ring {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] (B : Type u_3) [comm_ring B] [ B] [ B] (hS : S ) :

The canonical map from a localization of A at S to the fraction ring of A, given that S ≤ A⁰.

Equations
@[simp]
theorem localization.map_to_fraction_ring_apply {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] {B : Type u_3} [comm_ring B] [ B] [ B] (hS : S ) (b : B) :
hS) b =
theorem localization.mem_range_map_to_fraction_ring_iff {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] (B : Type u_3) [comm_ring B] [ B] [ B] (hS : S ) (x : K) :
x hS).range ∃ (a s : A) (hs : s S), x = s, _⟩
@[protected, instance]
def localization.is_localization_range_map_to_fraction_ring {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] (B : Type u_3) [comm_ring B] [ B] [ B] (hS : S ) :
hS).range)
@[protected, instance]
def localization.is_fraction_ring_range_map_to_fraction_ring {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] (B : Type u_3) [comm_ring B] [ B] [ B] (hS : S ) :
noncomputable def localization.subalgebra {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [ K] [ K] (hS : S ) :
K

Given a commutative ring A with fraction ring K, and a submonoid S of A which contains no zero divisor, this is the localization of A at S, considered as a subalgebra of K over A.

The carrier of this subalgebra is defined as the set of all x : K of the form is_localization.mk' K a ⟨s, _⟩, where s ∈ S.

Equations
Instances for ↥localization.subalgebra
@[protected, instance]
def localization.subalgebra.is_localization_subalgebra {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S ) [comm_ring K] [ K] [ K] :
hS)
@[protected, instance]
def localization.subalgebra.is_fraction_ring {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S ) [comm_ring K] [ K] [ K] :
K
theorem localization.subalgebra.mem_range_map_to_fraction_ring_iff_of_field {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S ) [field K] [ K] [ K] (B : Type u_3) [comm_ring B] [ B] [ B] (x : K) :
x hS).range ∃ (a s : A) (hs : s S), x = K) a * ( K) s)⁻¹
noncomputable def localization.subalgebra.of_field {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S ) [field K] [ K] [ K] :
K

Given a domain A with fraction field K, and a submonoid S of A which contains no zero divisor, this is the localization of A at S, considered as a subalgebra of K over A.

The carrier of this subalgebra is defined as the set of all x : K of the form algebra_map A K a * (algebra_map A K s)⁻¹ where a s : A and s ∈ S.

Equations
Instances for ↥localization.subalgebra.of_field
@[protected, instance]
def localization.subalgebra.is_localization_of_field {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S ) [field K] [ K] [ K] :
@[protected, instance]
def localization.subalgebra.is_fraction_ring_of_field {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S ) [field K] [ K] [ K] :