# 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_isUnit_of_le {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] (hS : ) (s : { x : A // x S }) :
IsUnit ((algebraMap A K) s)
noncomputable def Localization.mapToFractionRing {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] (B : Type u_3) [] [Algebra A B] [] (hS : ) :

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

Equations
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem Localization.mapToFractionRing_apply {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] {B : Type u_3} [] [Algebra A B] [] (hS : ) (b : B) :
b = b
theorem Localization.mem_range_mapToFractionRing_iff {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] (B : Type u_3) [] [Algebra A B] [] (hS : ) (x : K) :
x .range ∃ (a : A) (s : A) (hs : s S), x = IsLocalization.mk' K a s,
instance Localization.isLocalization_range_mapToFractionRing {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] (B : Type u_3) [] [Algebra A B] [] (hS : ) :
IsLocalization S { x : K // x .range }
Equations
• =
instance Localization.isFractionRing_range_mapToFractionRing {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] (B : Type u_3) [] [Algebra A B] [] (hS : ) :
IsFractionRing { x : K // x .range } K
Equations
• =
noncomputable def Localization.subalgebra {A : Type u_1} (K : Type u_2) [] (S : ) [] [Algebra A K] [] (hS : ) :

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 IsLocalization.mk' K a ⟨s, _⟩, where s ∈ S.

Equations
Instances For
instance Localization.subalgebra.isLocalization_subalgebra {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsLocalization S { x : K // x }
Equations
• =
instance Localization.subalgebra.isFractionRing {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsFractionRing { x : K // x } K
Equations
• =
theorem Localization.subalgebra.mem_range_mapToFractionRing_iff_ofField {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] (B : Type u_3) [] [Algebra A B] [] (x : K) :
x .range ∃ (a : A) (s : A) (_ : s S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
noncomputable def Localization.subalgebra.ofField {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A 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 algebraMap A K a * (algebraMap A K s)⁻¹ where a s : A and s ∈ S.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Localization.subalgebra.isLocalization_ofField {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsLocalization S { x : K // x }
Equations
• =
instance Localization.subalgebra.isFractionRing_ofField {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsFractionRing { x : K // x } K
Equations
• =