# Documentation

Mathlib.RingTheory.Localization.AsSubring

# 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 // x S }) :
IsUnit (↑() 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⁰.

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 = ↑(IsLocalization.lift (_ : ∀ (s : { x // x S }), IsUnit (↑() s))) 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 AlgHom.range () a s hs, x = IsLocalization.mk' K a { val := s, property := hS s hs }
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 : ) :
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 : ) :
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.

Instances For
instance Localization.subalgebra.isLocalization_subalgebra {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsLocalization S { x // x }
instance Localization.subalgebra.isFractionRing {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsFractionRing { x // x } K
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 AlgHom.range () a s x, x = ↑() a * (↑() 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.

Instances For
instance Localization.subalgebra.isLocalization_ofField {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsLocalization S { x // x }
instance Localization.subalgebra.isFractionRing_ofField {A : Type u_1} (K : Type u_2) [] (S : ) (hS : ) [] [Algebra A K] [] :
IsFractionRing { x // x } K